ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>a b : α<VAR>hf : Antitone f<GOAL>f (max a b) = min (f a) (f b)
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>a b : α<VAR>hf : Antitone f<GOAL>f (min a b) = max (f a) (f b)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>min a b = a ∨ min a b = b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>max a b = a ∨ max a b = b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<VAR>h : max a b ≤ c<GOAL>a ≤ c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<VAR>h : max a b ≤ c<GOAL>b ≤ c
<VAR>α : Type u<VAR>LinearOrder α<GOAL>Commutative max
<VAR>α : Type u<VAR>LinearOrder α<GOAL>Associative max
<VAR>α : Type u<VAR>LinearOrder α<GOAL>LeftCommutative max
<VAR>α : Type u<VAR>LinearOrder α<GOAL>Commutative min
<VAR>α : Type u<VAR>LinearOrder α<GOAL>Associative min
<VAR>α : Type u<VAR>LinearOrder α<GOAL>LeftCommutative min
<VAR>R : Type u_2<VAR>StrictOrderedSemiring R<VAR>Archimedean R<GOAL>Filter.comap Nat.cast Filter.atTop = Filter.atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>StrictOrderedSemiring R<VAR>Archimedean R<VAR>f : α → ℕ<VAR>l : Filter α<GOAL>Filter.Tendsto (fun n => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
<VAR>R : Type u_2<VAR>OrderedSemiring R<VAR>Archimedean R<GOAL>Filter.Tendsto Nat.cast Filter.atTop Filter.atTop
<VAR>R : Type u_2<VAR>OrderedSemiring R<VAR>Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in Filter.atTop, p x<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, p ↑n
<VAR>R : Type u_2<VAR>StrictOrderedRing R<VAR>Archimedean R<GOAL>Filter.comap Int.cast Filter.atTop = Filter.atTop
<VAR>R : Type u_2<VAR>StrictOrderedRing R<VAR>Archimedean R<GOAL>Filter.comap Int.cast Filter.atBot = Filter.atBot
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>StrictOrderedRing R<VAR>Archimedean R<VAR>f : α → ℤ<VAR>l : Filter α<GOAL>Filter.Tendsto (fun n => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>StrictOrderedRing R<VAR>Archimedean R<VAR>f : α → ℤ<VAR>l : Filter α<GOAL>Filter.Tendsto (fun n => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
<VAR>R : Type u_2<VAR>StrictOrderedRing R<VAR>Archimedean R<GOAL>Filter.Tendsto Int.cast Filter.atTop Filter.atTop
<VAR>R : Type u_2<VAR>StrictOrderedRing R<VAR>Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in Filter.atTop, p x<GOAL>∀ᶠ (n : ℤ) in Filter.atTop, p ↑n
<VAR>R : Type u_2<VAR>StrictOrderedRing R<VAR>Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in Filter.atBot, p x<GOAL>∀ᶠ (n : ℤ) in Filter.atBot, p ↑n
<VAR>R : Type u_2<VAR>LinearOrderedField R<VAR>Archimedean R<GOAL>Filter.comap Rat.cast Filter.atTop = Filter.atTop
<VAR>R : Type u_2<VAR>LinearOrderedField R<VAR>Archimedean R<GOAL>Filter.comap Rat.cast Filter.atBot = Filter.atBot
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedField R<VAR>Archimedean R<VAR>f : α → ℚ<VAR>l : Filter α<GOAL>Filter.Tendsto (fun n => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedField R<VAR>Archimedean R<VAR>f : α → ℚ<VAR>l : Filter α<GOAL>Filter.Tendsto (fun n => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
<VAR>R : Type u_2<VAR>LinearOrderedField R<VAR>Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in Filter.atTop, p x<GOAL>∀ᶠ (n : ℚ) in Filter.atTop, p ↑n
<VAR>R : Type u_2<VAR>LinearOrderedField R<VAR>Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in Filter.atBot, p x<GOAL>∀ᶠ (n : ℚ) in Filter.atBot, p ↑n
<VAR>R : Type u_2<VAR>OrderedSemiring R<VAR>Archimedean R<GOAL>Filter.atTop.HasAntitoneBasis fun n => Set.Ici ↑n
<VAR>R : Type u_2<VAR>StrictOrderedSemiring R<VAR>Archimedean R<GOAL>Filter.atTop.HasCountableBasis (fun x => True) fun n => Set.Ici ↑n
<VAR>R : Type u_2<VAR>LinearOrderedRing R<VAR>Archimedean R<GOAL>Filter.atBot.HasCountableBasis (fun x => True) fun m => Set.Iic ↑m
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>LinearOrderedSemiring R<VAR>Archimedean R<VAR>hr : 0 < r<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => r * f x) l Filter.atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>LinearOrderedSemiring R<VAR>Archimedean R<VAR>hr : 0 < r<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>LinearOrderedRing R<VAR>Archimedean R<VAR>hr : r < 0<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atBot
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>LinearOrderedRing R<VAR>Archimedean R<VAR>hr : 0 < r<VAR>hf : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atBot
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>LinearOrderedRing R<VAR>Archimedean R<VAR>hr : r < 0<VAR>hf : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x * r) l Filter.atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>r : R<VAR>LinearOrderedCancelAddCommMonoid R<VAR>Archimedean R<VAR>f : α → ℕ<VAR>hr : 0 < r<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x • r) l Filter.atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>r : R<VAR>LinearOrderedAddCommGroup R<VAR>Archimedean R<VAR>f : α → ℕ<VAR>hr : r < 0<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x • r) l Filter.atBot
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>r : R<VAR>LinearOrderedAddCommGroup R<VAR>Archimedean R<VAR>f : α → ℤ<VAR>hr : 0 < r<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x • r) l Filter.atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>r : R<VAR>LinearOrderedAddCommGroup R<VAR>Archimedean R<VAR>f : α → ℤ<VAR>hr : r < 0<VAR>hf : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (fun x => f x • r) l Filter.atBot
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>r : R<VAR>LinearOrderedAddCommGroup R<VAR>Archimedean R<VAR>f : α → ℤ<VAR>hr : 0 < r<VAR>hf : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x • r) l Filter.atBot
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>r : R<VAR>LinearOrderedAddCommGroup R<VAR>Archimedean R<VAR>f : α → ℤ<VAR>hr : r < 0<VAR>hf : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (fun x => f x • r) l Filter.atTop
<VAR>α : Type u_2<VAR>r : α → α → Prop<GOAL>∅.WellFoundedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>s.WellFoundedOn r ↔ WellFounded fun a b => r a b ∧ a ∈ s ∧ b ∈ s
<VAR>α : Type u_2<VAR>r : α → α → Prop<GOAL>Set.univ.WellFoundedOn r ↔ WellFounded r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>WellFounded r → s.WellFoundedOn r
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → α → Prop<VAR>f : β → α<GOAL>(Set.range f).WellFoundedOn r ↔ WellFounded (r on f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → α → Prop<VAR>f : β → α<VAR>s : Set β<GOAL>(f '' s).WellFoundedOn r ↔ s.WellFoundedOn (r on f)
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<VAR>x : α<VAR>hs : s.WellFoundedOn r<VAR>hx : x ∈ s<VAR>P : α → Prop<VAR>hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y<GOAL>P x
<VAR>α : Type u_2<VAR>r r' : α → α → Prop<VAR>s t : Set α<VAR>h : t.WellFoundedOn r'<VAR>hle : r ≤ r'<VAR>hst : s ⊆ t<GOAL>s.WellFoundedOn r
<VAR>α : Type u_2<VAR>r r' : α → α → Prop<VAR>s : Set α<VAR>h : ∀ a ∈ s, ∀ b ∈ s, r' a b → r a b<GOAL>s.WellFoundedOn r → s.WellFoundedOn r'
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>h : t.WellFoundedOn r<VAR>hst : s ⊆ t<GOAL>s.WellFoundedOn r
<VAR>α : Type u_6<VAR>r : α → α → Prop<VAR>a : α<GOAL>[Acc r a, {b | Relation.ReflTransGen r b a}.WellFoundedOn r, {b | Relation.TransGen r b a}.WellFoundedOn r].TFAE
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>s : Set α<GOAL>s.WellFoundedOn r ↔ ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ℕ), f n ∈ s
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>s t : Set α<VAR>hs : s.WellFoundedOn r<VAR>ht : t.WellFoundedOn r<GOAL>(s ∪ t).WellFoundedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>s t : Set α<GOAL>(s ∪ t).WellFoundedOn r ↔ s.WellFoundedOn r ∧ t.WellFoundedOn r
<VAR>α : Type u_2<VAR>LT α<GOAL>∅.IsWF
<VAR>α : Type u_2<VAR>LT α<GOAL>Set.univ.IsWF ↔ WellFounded fun x x_1 => x < x_1
<VAR>α : Type u_2<VAR>LT α<VAR>s t : Set α<VAR>h : t.IsWF<VAR>st : s ⊆ t<GOAL>s.IsWF
<VAR>α : Type u_2<VAR>Preorder α<VAR>s t : Set α<VAR>hs : s.IsWF<VAR>ht : t.IsWF<GOAL>(s ∪ t).IsWF
<VAR>α : Type u_2<VAR>Preorder α<VAR>s t : Set α<GOAL>(s ∪ t).IsWF ↔ s.IsWF ∧ t.IsWF
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<GOAL>s.IsWF ↔ ∀ (f : ℕ → α), StrictAnti f → ¬∀ (n : ℕ), f (OrderDual.toDual n) ∈ s
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>ht : t.PartiallyWellOrderedOn r<VAR>h : s ⊆ t<GOAL>s.PartiallyWellOrderedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<GOAL>∅.PartiallyWellOrderedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>hs : s.PartiallyWellOrderedOn r<VAR>ht : t.PartiallyWellOrderedOn r<GOAL>(s ∪ t).PartiallyWellOrderedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s t : Set α<GOAL>(s ∪ t).PartiallyWellOrderedOn r ↔ s.PartiallyWellOrderedOn r ∧ t.PartiallyWellOrderedOn r
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s : Set α<VAR>hs : s.PartiallyWellOrderedOn r<VAR>hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)<GOAL>(f '' s).PartiallyWellOrderedOn r'
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<VAR>ha : IsAntichain r s<VAR>hp : s.PartiallyWellOrderedOn r<GOAL>s.Finite
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsRefl α r<VAR>hs : s.Finite<GOAL>s.PartiallyWellOrderedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsRefl α r<VAR>hs : IsAntichain r s<GOAL>s.PartiallyWellOrderedOn r ↔ s.Finite
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>a : α<GOAL>{a}.PartiallyWellOrderedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsRefl α r<VAR>hs : s.Subsingleton<GOAL>s.PartiallyWellOrderedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>IsRefl α r<GOAL>(insert a s).PartiallyWellOrderedOn r ↔ s.PartiallyWellOrderedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsRefl α r<VAR>h : s.PartiallyWellOrderedOn r<VAR>a : α<GOAL>(insert a s).PartiallyWellOrderedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsRefl α r<VAR>IsSymm α r<GOAL>s.PartiallyWellOrderedOn r ↔ ∀ t ⊆ s, IsAntichain r t → t.Finite
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsRefl α r<VAR>IsTrans α r<VAR>h : s.PartiallyWellOrderedOn r<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<GOAL>∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsRefl α r<VAR>IsTrans α r<GOAL>s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>s : Set α<VAR>IsRefl α r<VAR>IsTrans α r<VAR>t : Set β<VAR>hs : s.PartiallyWellOrderedOn r<VAR>ht : t.PartiallyWellOrderedOn r'<GOAL>(s ×ˢ t).PartiallyWellOrderedOn fun x y => r x.1 y.1 ∧ r' x.2 y.2
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsPreorder α r<VAR>h : s.PartiallyWellOrderedOn r<GOAL>s.WellFoundedOn fun a b => r a b ∧ ¬r b a
<VAR>α : Type u_2<VAR>Preorder α<VAR>s t : Set α<VAR>ht : t.IsPWO<GOAL>s ⊆ t → s.IsPWO
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>h : s.IsPWO<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), f n ∈ s<GOAL>∃ g, Monotone (f ∘ ⇑g)
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<GOAL>s.IsPWO ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, Monotone (f ∘ ⇑g)
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>h : s.IsPWO<GOAL>s.IsWF
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>(s ×ˢ t).IsPWO
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>hs : s.IsPWO<VAR>f : α → β<VAR>hf : MonotoneOn f s<GOAL>(f '' s).IsPWO
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>hs : s.IsPWO<VAR>f : α → β<VAR>hf : Monotone f<GOAL>(f '' s).IsPWO
<VAR>α : Type u_2<VAR>Preorder α<VAR>s t : Set α<VAR>hs : s.IsPWO<VAR>ht : t.IsPWO<GOAL>(s ∪ t).IsPWO
<VAR>α : Type u_2<VAR>Preorder α<VAR>s t : Set α<GOAL>(s ∪ t).IsPWO ↔ s.IsPWO ∧ t.IsPWO
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>s.IsPWO
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>Finite α<GOAL>s.IsPWO
<VAR>α : Type u_2<VAR>Preorder α<VAR>a : α<GOAL>{a}.IsPWO
<VAR>α : Type u_2<VAR>Preorder α<GOAL>∅.IsPWO
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>s.IsPWO
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>a : α<GOAL>(insert a s).IsPWO ↔ s.IsPWO
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>h : s.IsPWO<VAR>a : α<GOAL>(insert a s).IsPWO
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>s.IsWF
<VAR>α : Type u_2<VAR>Preorder α<VAR>a : α<GOAL>{a}.IsWF
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>s.IsWF
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>a : α<GOAL>(insert a s).IsWF ↔ s.IsWF
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>h : s.IsWF<VAR>a : α<GOAL>(insert a s).IsWF
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>s : Set α<VAR>hs : s.Finite<GOAL>s.WellFoundedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>a : α<GOAL>{a}.WellFoundedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>s.WellFoundedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>s : Set α<VAR>a : α<GOAL>(insert a s).WellFoundedOn r ↔ s.WellFoundedOn r
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>s : Set α<VAR>h : s.WellFoundedOn r<VAR>a : α<GOAL>(insert a s).WellFoundedOn r
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Set α<VAR>hs : s.IsWF<GOAL>s.IsPWO
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Set α<GOAL>s.IsWF ↔ s.IsPWO
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>s : Finset α<GOAL>(↑s).PartiallyWellOrderedOn r
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Finset α<GOAL>(↑s).IsPWO
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Finset α<GOAL>(↑s).IsWF
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>s : Finset α<GOAL>(↑s).WellFoundedOn r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>(s.sup f).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>(s.sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>(s.sup f).IsWF ↔ ∀ i ∈ s, (f i).IsWF
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>(s.sup f).IsPWO ↔ ∀ i ∈ s, (f i).IsPWO
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsStrictOrder α r<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>(⋃ i ∈ s, f i).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>(⋃ i ∈ s, f i).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>(⋃ i ∈ s, f i).IsWF ↔ ∀ i ∈ s, (f i).IsWF
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>(⋃ i ∈ s, f i).IsPWO ↔ ∀ i ∈ s, (f i).IsPWO
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>hs : s.IsWF<VAR>hn : s.Nonempty<GOAL>hs.min hn ∈ s
<VAR>α : Type u_2<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>hs : s.IsWF<VAR>hn : s.Nonempty<VAR>ha : a ∈ s<GOAL>¬a < hs.min hn
<VAR>α : Type u_2<VAR>Preorder α<VAR>s t : Set α<VAR>hs : s.IsWF<VAR>hsn : s.Nonempty<VAR>ht : t.IsWF<VAR>htn : t.Nonempty<VAR>hst : s ⊆ t<GOAL>¬hs.min hsn < ht.min htn
<VAR>α : Type u_2<VAR>Preorder α<VAR>a : α<VAR>hs : {a}.IsWF<VAR>hn : {a}.Nonempty<GOAL>hs.min hn = a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>hs : s.IsWF<VAR>hn : s.Nonempty<VAR>ha : a ∈ s<GOAL>hs.min hn ≤ a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>hs : s.IsWF<VAR>hn : s.Nonempty<GOAL>a ≤ hs.min hn ↔ ∀ b ∈ s, a ≤ b
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s t : Set α<VAR>hs : s.IsWF<VAR>hsn : s.Nonempty<VAR>ht : t.IsWF<VAR>htn : t.Nonempty<VAR>hst : s ⊆ t<GOAL>ht.min htn ≤ hs.min hsn
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s t : Set α<VAR>hs : s.IsWF<VAR>hsn : s.Nonempty<VAR>ht : t.IsWF<VAR>htn : t.Nonempty<GOAL>⋯.min ⋯ = min (hs.min hsn) (ht.min htn)
<VAR>α : Type u_2<VAR>s : Set α<VAR>Preorder α<VAR>LocallyFiniteOrder α<GOAL>BddBelow s → s.WellFoundedOn fun x x_1 => x < x_1
<VAR>α : Type u_2<VAR>s : Set α<VAR>Preorder α<VAR>LocallyFiniteOrder α<GOAL>BddAbove s → s.WellFoundedOn fun x x_1 => x > x_1
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), ¬Set.PartiallyWellOrderedOn.IsBadSeq r s f
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>rk : α → ℕ<VAR>s : Set α<GOAL>(∃ f, Set.PartiallyWellOrderedOn.IsBadSeq r s f) → ∃ f, Set.PartiallyWellOrderedOn.IsBadSeq r s f ∧ ∀ (n : ℕ), Set.PartiallyWellOrderedOn.IsMinBadSeq r rk s n f
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>rk : α → ℕ<VAR>s : Set α<GOAL>s.PartiallyWellOrderedOn r ↔ ¬∃ f, Set.PartiallyWellOrderedOn.IsBadSeq r s f ∧ ∀ (n : ℕ), Set.PartiallyWellOrderedOn.IsMinBadSeq r rk s n f
<VAR>α : Type u_2<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>IsTrans α r<VAR>s : Set α<VAR>h : s.PartiallyWellOrderedOn r<GOAL>{l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>Preorder β<VAR>s : Set (Lex (α × β))<VAR>hα : ((fun x => (ofLex x).1) '' s).IsPWO<VAR>hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO<GOAL>s.IsPWO
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>Preorder β<VAR>s : Set (Lex (α × β))<VAR>hαβ : s.IsPWO<GOAL>((fun x => (ofLex x).1) '' s).IsPWO
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>Preorder β<VAR>s : Set (Lex (α × β))<VAR>hαβ : s.IsPWO<VAR>a : α<GOAL>{y | toLex (a, y) ∈ s}.IsPWO
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PartialOrder α<VAR>Preorder β<VAR>s : Set (Lex (α × β))<GOAL>s.IsPWO ↔ ((fun x => (ofLex x).1) '' s).IsPWO ∧ ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
<VAR>α : Type u_2<VAR>LT α<VAR>h : WellFounded fun x x_1 => x < x_1<VAR>s : Set α<GOAL>s.IsWF
<VAR>ι : Type u_1<VAR>α : ι → Type u_6<VAR>(i : ι) → LinearOrder (α i)<VAR>∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1<VAR>Finite ι<VAR>s : Set ((i : ι) → α i)<GOAL>s.IsPWO
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>f : γ → α<VAR>g : γ → β<VAR>hα : WellFounded (rα on f)<VAR>hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)<GOAL>WellFounded (Prod.Lex rα rβ on fun c => (f c, g c))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>f : γ → α<VAR>g : γ → β<VAR>s : Set γ<VAR>hα : s.WellFoundedOn (rα on f)<VAR>hβ : ∀ (a : α), (s ∩ f ⁻¹' {a}).WellFoundedOn (rβ on g)<GOAL>s.WellFoundedOn (Prod.Lex rα rβ on fun c => (f c, g c))
<VAR>ι : Type u_1<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>rι : ι → ι → Prop<VAR>rπ : (i : ι) → π i → π i → Prop<VAR>f : γ → ι<VAR>g : (i : ι) → γ → π i<VAR>hι : WellFounded (rι on f)<VAR>hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)<GOAL>WellFounded (Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) c⟩)
<VAR>ι : Type u_1<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>rι : ι → ι → Prop<VAR>rπ : (i : ι) → π i → π i → Prop<VAR>f : γ → ι<VAR>g : (i : ι) → γ → π i<VAR>s : Set γ<VAR>hι : s.WellFoundedOn (rι on f)<VAR>hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)<GOAL>s.WellFoundedOn (Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) c⟩)
<GOAL>(fun x x_1 => x ⊔ x_1) = fun x x_1 => x ∨ x_1
<GOAL>(fun x x_1 => x ⊓ x_1) = fun x x_1 => x ∧ x_1
<VAR>ι : Type u_1<VAR>α' : ι → Type u_2<VAR>(i : ι) → PartialOrder (α' i)<VAR>(i : ι) → OrderBot (α' i)<VAR>f g : (i : ι) → α' i<GOAL>Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)
<VAR>ι : Type u_1<VAR>α' : ι → Type u_2<VAR>(i : ι) → PartialOrder (α' i)<VAR>(i : ι) → OrderTop (α' i)<VAR>f g : (i : ι) → α' i<GOAL>Codisjoint f g ↔ ∀ (i : ι), Codisjoint (f i) (g i)
<VAR>ι : Type u_1<VAR>α' : ι → Type u_2<VAR>(i : ι) → PartialOrder (α' i)<VAR>(i : ι) → BoundedOrder (α' i)<VAR>f g : (i : ι) → α' i<GOAL>IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)
<VAR>P Q : Prop<GOAL>Disjoint P Q ↔ ¬(P ∧ Q)
<VAR>P Q : Prop<GOAL>Codisjoint P Q ↔ P ∨ Q
<VAR>P : Type u_2<VAR>LE P<VAR>self : Order.Ideal P<GOAL>DirectedOn (fun x x_1 => x ≤ x_1) self.carrier
<VAR>P : Type u_2<VAR>LE P<VAR>self : Order.Ideal P<GOAL>self.carrier.Nonempty
<VAR>P : Type u_2<VAR>LE P<VAR>I : Set P<VAR>self : Order.IsIdeal I<GOAL>I.Nonempty
<VAR>P : Type u_2<VAR>LE P<VAR>I : Set P<VAR>self : Order.IsIdeal I<GOAL>IsLowerSet I
<VAR>P : Type u_2<VAR>LE P<VAR>I : Set P<VAR>self : Order.IsIdeal I<GOAL>DirectedOn (fun x x_1 => x ≤ x_1) I
<VAR>P : Type u_2<VAR>LE P<VAR>I : Set P<GOAL>Order.IsIdeal I ↔ IsLowerSet I ∧ I.Nonempty ∧ DirectedOn (fun x x_1 => x ≤ x_1) I
<VAR>P : Type u_1<VAR>LE P<GOAL>Function.Injective Order.Ideal.toLowerSet
<VAR>P : Type u_1<VAR>LE P<VAR>s t : Order.Ideal P<GOAL>↑s = ↑t → s = t
<VAR>P : Type u_1<VAR>LE P<VAR>s : Order.Ideal P<GOAL>s.carrier = ↑s
<VAR>P : Type u_1<VAR>LE P<VAR>s : Order.Ideal P<GOAL>↑s.toLowerSet = ↑s
<VAR>P : Type u_1<VAR>LE P<VAR>s : Order.Ideal P<GOAL>IsLowerSet ↑s
<VAR>P : Type u_1<VAR>LE P<VAR>s : Order.Ideal P<GOAL>(↑s).Nonempty
<VAR>P : Type u_1<VAR>LE P<VAR>s : Order.Ideal P<GOAL>DirectedOn (fun x x_1 => x ≤ x_1) ↑s
<VAR>P : Type u_1<VAR>LE P<VAR>s : Order.Ideal P<GOAL>Order.IsIdeal ↑s
<VAR>P : Type u_1<VAR>LE P<VAR>I : Order.Ideal P<VAR>x y : P<GOAL>x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ
<VAR>P : Type u_1<VAR>LE P<VAR>s t : Order.Ideal P<GOAL>↑s ⊆ ↑t ↔ s ≤ t
<VAR>P : Type u_1<VAR>LE P<VAR>s t : Order.Ideal P<GOAL>↑s ⊂ ↑t ↔ s < t
<VAR>P : Type u_1<VAR>LE P<VAR>x : P<VAR>I J : Order.Ideal P<GOAL>x ∈ I → I ≤ J → x ∈ J
<VAR>P : Type u_1<VAR>LE P<VAR>I : Order.Ideal P<GOAL>I.IsProper ↔ ↑I ≠ Set.univ
<VAR>P : Type u_1<VAR>LE P<VAR>I : Order.Ideal P<VAR>self : I.IsProper<GOAL>↑I ≠ Set.univ
<VAR>P : Type u_1<VAR>LE P<VAR>I : Order.Ideal P<VAR>p : P<VAR>nmem : p ∉ I<GOAL>I.IsProper
<VAR>P : Type u_1<VAR>LE P<VAR>I : Order.Ideal P<GOAL>I.IsMaximal ↔ I.IsProper ∧ ∀ ⦃J : Order.Ideal P⦄, I < J → ↑J = Set.univ
<VAR>P : Type u_1<VAR>LE P<VAR>I : Order.Ideal P<VAR>self : I.IsMaximal<VAR>J : Order.Ideal P<GOAL>I < J → ↑J = Set.univ
<VAR>P : Type u_1<VAR>LE P<VAR>IsDirected P fun x x_1 => x ≥ x_1<VAR>I J : Order.Ideal P<GOAL>(↑I ∩ ↑J).Nonempty
<VAR>P : Type u_1<VAR>LE P<VAR>IsDirected P fun x x_1 => x ≤ x_1<VAR>Nonempty P<GOAL>⊤.toLowerSet = ⊤
<VAR>P : Type u_1<VAR>LE P<VAR>IsDirected P fun x x_1 => x ≤ x_1<VAR>Nonempty P<GOAL>↑⊤ = Set.univ
<VAR>P : Type u_1<VAR>LE P<VAR>IsDirected P fun x x_1 => x ≤ x_1<VAR>Nonempty P<VAR>I : Order.Ideal P<VAR>ne_top : I ≠ ⊤<GOAL>I.IsProper
<VAR>P : Type u_1<VAR>LE P<VAR>IsDirected P fun x x_1 => x ≤ x_1<VAR>Nonempty P<VAR>I : Order.Ideal P<GOAL>I.IsProper → I ≠ ⊤
<VAR>P : Type u_1<VAR>LE P<VAR>IsDirected P fun x x_1 => x ≤ x_1<VAR>Nonempty P<VAR>I : Order.Ideal P<VAR>hI : IsCoatom I<GOAL>I.IsProper
<VAR>P : Type u_1<VAR>LE P<VAR>IsDirected P fun x x_1 => x ≤ x_1<VAR>Nonempty P<VAR>I : Order.Ideal P<GOAL>I.IsProper ↔ I ≠ ⊤
<VAR>P : Type u_1<VAR>LE P<VAR>IsDirected P fun x x_1 => x ≤ x_1<VAR>Nonempty P<VAR>I : Order.Ideal P<GOAL>I.IsMaximal → IsCoatom I
<VAR>P : Type u_1<VAR>LE P<VAR>IsDirected P fun x x_1 => x ≤ x_1<VAR>Nonempty P<VAR>I : Order.Ideal P<VAR>I.IsMaximal<GOAL>IsCoatom I
<VAR>P : Type u_1<VAR>LE P<VAR>IsDirected P fun x x_1 => x ≤ x_1<VAR>Nonempty P<VAR>I : Order.Ideal P<VAR>hI : IsCoatom I<GOAL>I.IsMaximal
<VAR>P : Type u_1<VAR>LE P<VAR>IsDirected P fun x x_1 => x ≤ x_1<VAR>Nonempty P<VAR>I : Order.Ideal P<GOAL>I.IsMaximal ↔ IsCoatom I
<VAR>P : Type u_1<VAR>LE P<VAR>OrderBot P<VAR>s : Order.Ideal P<GOAL>⊥ ∈ s
<VAR>P : Type u_1<VAR>LE P<VAR>OrderTop P<VAR>I : Order.Ideal P<VAR>h : ⊤ ∈ I<GOAL>I = ⊤