ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>P : Type u_1<VAR>LE P<VAR>OrderTop P<VAR>I : Order.Ideal P<VAR>hI : I.IsProper<GOAL>⊤ ∉ I
<VAR>P : Type u_1<VAR>Preorder P<VAR>p : P<GOAL>(Order.Ideal.principal p).toLowerSet = LowerSet.Iic p
<VAR>P : Type u_1<VAR>Preorder P<VAR>I : Order.Ideal P<VAR>x : P<GOAL>Order.Ideal.principal x ≤ I ↔ x ∈ I
<VAR>P : Type u_1<VAR>Preorder P<VAR>x y : P<GOAL>x ∈ Order.Ideal.principal y ↔ x ≤ y
<VAR>P : Type u_1<VAR>Preorder P<VAR>x : P<GOAL>x ∈ Order.Ideal.principal x
<VAR>P : Type u_1<VAR>Preorder P<VAR>OrderBot P<GOAL>Order.Ideal.principal ⊥ = ⊥
<VAR>P : Type u_1<VAR>Preorder P<VAR>OrderTop P<GOAL>Order.Ideal.principal ⊤ = ⊤
<VAR>P : Type u_1<VAR>SemilatticeSup P<VAR>x y : P<VAR>s : Order.Ideal P<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x ⊔ y ∈ s
<VAR>P : Type u_1<VAR>SemilatticeSup P<VAR>x y : P<VAR>I : Order.Ideal P<GOAL>x ⊔ y ∈ I ↔ x ∈ I ∧ y ∈ I
<VAR>P : Type u_1<VAR>SemilatticeSup P<VAR>IsDirected P fun x x_1 => x ≥ x_1<VAR>s t : Order.Ideal P<GOAL>↑(s ⊔ t) = {x | ∃ a ∈ s, ∃ b ∈ t, x ≤ a ⊔ b}
<VAR>P : Type u_1<VAR>SemilatticeSup P<VAR>IsDirected P fun x x_1 => x ≥ x_1<VAR>s t : Order.Ideal P<GOAL>↑(s ⊓ t) = ↑s ∩ ↑t
<VAR>P : Type u_1<VAR>SemilatticeSup P<VAR>IsDirected P fun x x_1 => x ≥ x_1<VAR>x : P<VAR>I J : Order.Ideal P<GOAL>x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J
<VAR>P : Type u_1<VAR>SemilatticeSup P<VAR>IsDirected P fun x x_1 => x ≥ x_1<VAR>x : P<VAR>I J : Order.Ideal P<GOAL>x ∈ I ⊔ J ↔ ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j
<VAR>P : Type u_1<VAR>SemilatticeSup P<VAR>IsDirected P fun x x_1 => x ≥ x_1<VAR>x : P<VAR>I : Order.Ideal P<VAR>hx : x ∉ I<GOAL>I < I ⊔ Order.Ideal.principal x
<VAR>P : Type u_1<VAR>SemilatticeSup P<VAR>OrderBot P<VAR>S : Set (Order.Ideal P)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>P : Type u_1<VAR>SemilatticeSup P<VAR>OrderBot P<VAR>x : P<VAR>S : Set (Order.Ideal P)<GOAL>x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s
<VAR>P : Type u_1<VAR>DistribLattice P<VAR>I J : Order.Ideal P<VAR>x i j : P<VAR>hi : i ∈ I<VAR>hj : j ∈ J<VAR>hx : x ≤ i ⊔ j<GOAL>∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'
<VAR>P : Type u_1<VAR>DistribLattice P<VAR>I J : Order.Ideal P<GOAL>↑(I ⊔ J) = {x | ∃ i ∈ I, ∃ j ∈ J, x = i ⊔ j}
<VAR>P : Type u_1<VAR>BooleanAlgebra P<VAR>x : P<VAR>I : Order.Ideal P<VAR>hI : I.IsProper<VAR>hxc : xᶜ ∈ I<GOAL>x ∉ I
<VAR>P : Type u_1<VAR>BooleanAlgebra P<VAR>x : P<VAR>I : Order.Ideal P<VAR>hI : I.IsProper<GOAL>x ∉ I ∨ xᶜ ∉ I
<VAR>P : Type u_2<VAR>Preorder P<VAR>self : Order.Cofinal P<VAR>x : P<GOAL>∃ y ∈ self.carrier, x ≤ y
<VAR>P : Type u_1<VAR>Preorder P<VAR>D : Order.Cofinal P<VAR>x : P<GOAL>D.above x ∈ D
<VAR>P : Type u_1<VAR>Preorder P<VAR>D : Order.Cofinal P<VAR>x : P<GOAL>x ≤ D.above x
<VAR>P : Type u_1<VAR>Preorder P<VAR>p : P<VAR>ι : Type u_2<VAR>Encodable ι<VAR>𝒟 : ι → Order.Cofinal P<GOAL>Monotone (Order.sequenceOfCofinals p 𝒟)
<VAR>P : Type u_1<VAR>Preorder P<VAR>p : P<VAR>ι : Type u_2<VAR>Encodable ι<VAR>𝒟 : ι → Order.Cofinal P<VAR>i : ι<GOAL>Order.sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i
<VAR>P : Type u_1<VAR>Preorder P<VAR>p : P<VAR>ι : Type u_2<VAR>Encodable ι<VAR>𝒟 : ι → Order.Cofinal P<GOAL>p ∈ Order.idealOfCofinals p 𝒟
<VAR>P : Type u_1<VAR>Preorder P<VAR>p : P<VAR>ι : Type u_2<VAR>Encodable ι<VAR>𝒟 : ι → Order.Cofinal P<VAR>i : ι<GOAL>∃ x ∈ 𝒟 i, x ∈ Order.idealOfCofinals p 𝒟
<VAR>P : Type u_1<VAR>Preorder P<VAR>C : Set (Set P)<VAR>hidl : ∀ I ∈ C, Order.IsIdeal I<VAR>hD : DirectedOn (fun x x_1 => x ⊆ x_1) C<VAR>hNe : C.Nonempty<GOAL>Order.IsIdeal (⋃₀ C)
<VAR>P : Type u_1<VAR>Preorder P<VAR>C : Set (Set P)<VAR>hidl : ∀ I ∈ C, Order.IsIdeal I<VAR>hC : IsChain (fun x x_1 => x ⊆ x_1) C<VAR>hNe : C.Nonempty<GOAL>Order.IsIdeal (⋃₀ C)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub<VAR>trans : ∀ {a b c : α}, r a b → r b c → r a c<GOAL>∃ m, ∀ (a : α), r m a → r a m
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>Nonempty α<VAR>h : ∀ (c : Set α), IsChain r c → c.Nonempty → ∃ ub, ∀ a ∈ c, r a ub<VAR>trans : ∀ {a b c : α}, r a b → r b c → r a c<GOAL>∃ m, ∀ (a : α), r m a → r a m
<VAR>α : Type u_1<VAR>Preorder α<VAR>h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → BddAbove c<GOAL>∃ m, ∀ (a : α), m ≤ a → a ≤ m
<VAR>α : Type u_1<VAR>Preorder α<VAR>Nonempty α<VAR>h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → c.Nonempty → BddAbove c<GOAL>∃ m, ∀ (a : α), m ≤ a → a ≤ m
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>ih : ∀ c ⊆ s, IsChain (fun x x_1 => x ≤ x_1) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub<GOAL>∃ m ∈ s, ∀ z ∈ s, m ≤ z → z ≤ m
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>ih : ∀ c ⊆ s, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub<VAR>x : α<VAR>hxs : x ∈ s<GOAL>∃ m ∈ s, x ≤ m ∧ ∀ z ∈ s, m ≤ z → z ≤ m
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<VAR>ih : ∀ c ⊆ Set.Ici a, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub<VAR>x : α<VAR>hax : a ≤ x<GOAL>∃ m, x ≤ m ∧ ∀ (z : α), m ≤ z → z ≤ m
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → BddAbove c<GOAL>∃ m, ∀ (a : α), m ≤ a → a = m
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>Nonempty α<VAR>h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → c.Nonempty → BddAbove c<GOAL>∃ m, ∀ (a : α), m ≤ a → a = m
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Set α<VAR>ih : ∀ c ⊆ s, IsChain (fun x x_1 => x ≤ x_1) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub<GOAL>∃ m ∈ s, ∀ z ∈ s, m ≤ z → z = m
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Set α<VAR>ih : ∀ c ⊆ s, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub<VAR>x : α<VAR>hxs : x ∈ s<GOAL>∃ m ∈ s, x ≤ m ∧ ∀ z ∈ s, m ≤ z → z = m
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>h : ∀ c ⊆ S, IsChain (fun x x_1 => x ⊆ x_1) c → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub<GOAL>∃ m ∈ S, ∀ a ∈ S, m ⊆ a → a = m
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>H : ∀ c ⊆ S, IsChain (fun x x_1 => x ⊆ x_1) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub<VAR>x : Set α<VAR>hx : x ∈ S<GOAL>∃ m ∈ S, x ⊆ m ∧ ∀ a ∈ S, m ⊆ a → a = m
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>h : ∀ c ⊆ S, IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s<GOAL>∃ m ∈ S, ∀ a ∈ S, a ⊆ m → a = m
<VAR>α : Type u_1<VAR>S : Set (Set α)<VAR>H : ∀ c ⊆ S, IsChain (fun x x_1 => x ⊆ x_1) c → c.Nonempty → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s<VAR>x : Set α<VAR>hx : x ∈ S<GOAL>∃ m ∈ S, m ⊆ x ∧ ∀ a ∈ S, a ⊆ m → a = m
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Set α<VAR>hc : IsChain r c<GOAL>∃ M, IsMaxChain r M ∧ c ⊆ M
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<VAR>ha : SupIrred a<GOAL>¬IsMin a
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<VAR>ha : SupPrime a<GOAL>¬IsMin a
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<VAR>ha : IsMin a<GOAL>¬SupIrred a
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<VAR>ha : IsMin a<GOAL>¬SupPrime a
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<GOAL>¬SupIrred a ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<GOAL>¬SupPrime a ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<GOAL>SupPrime a → SupIrred a
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a b c : α<VAR>ha : SupPrime a<GOAL>a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>OrderBot α<GOAL>¬SupIrred ⊥
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>OrderBot α<GOAL>¬SupPrime ⊥
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<VAR>OrderBot α<VAR>ha : SupIrred a<GOAL>a ≠ ⊥
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<VAR>OrderBot α<VAR>ha : SupPrime a<GOAL>a ≠ ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>ha : SupIrred a<VAR>h : s.sup f = a<GOAL>∃ i ∈ s, f i = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>ha : SupPrime a<GOAL>a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>OrderBot α<VAR>WellFoundedLT α<VAR>a : α<GOAL>∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<VAR>ha : IsMax a<GOAL>¬InfIrred a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<VAR>ha : IsMax a<GOAL>¬InfPrime a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<GOAL>¬InfIrred a ↔ IsMax a ∨ ∃ b c, b ⊓ c = a ∧ a < b ∧ a < c
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<GOAL>¬InfPrime a ↔ IsMax a ∨ ∃ b c, b ⊓ c ≤ a ∧ ¬b ≤ a ∧ ¬c ≤ a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<GOAL>InfPrime a → InfIrred a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a b c : α<VAR>ha : InfPrime a<GOAL>b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>OrderTop α<GOAL>¬InfIrred ⊤
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>OrderTop α<GOAL>¬InfPrime ⊤
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<VAR>OrderTop α<VAR>ha : InfIrred a<GOAL>a ≠ ⊤
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<VAR>OrderTop α<VAR>ha : InfPrime a<GOAL>a ≠ ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<VAR>OrderTop α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>InfIrred a → s.inf f = a → ∃ i ∈ s, f i = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<VAR>OrderTop α<VAR>s : Finset ι<VAR>f : ι → α<VAR>ha : InfPrime a<GOAL>s.inf f ≤ a ↔ ∃ i ∈ s, f i ≤ a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>OrderTop α<VAR>WellFoundedGT α<VAR>a : α<GOAL>∃ s, s.inf id = a ∧ ∀ ⦃b : α⦄, b ∈ s → InfIrred b
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<GOAL>InfIrred (OrderDual.toDual a) ↔ SupIrred a
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<GOAL>InfPrime (OrderDual.toDual a) ↔ SupPrime a
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : αᵒᵈ<GOAL>SupIrred (OrderDual.ofDual a) ↔ InfIrred a
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : αᵒᵈ<GOAL>SupPrime (OrderDual.ofDual a) ↔ InfPrime a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<GOAL>SupIrred (OrderDual.toDual a) ↔ InfIrred a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<GOAL>SupPrime (OrderDual.toDual a) ↔ InfPrime a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : αᵒᵈ<GOAL>InfIrred (OrderDual.ofDual a) ↔ SupIrred a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : αᵒᵈ<GOAL>InfPrime (OrderDual.ofDual a) ↔ SupPrime a
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>a : α<GOAL>SupPrime a ↔ SupIrred a
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>a : α<GOAL>InfPrime a ↔ InfIrred a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<GOAL>SupPrime a ↔ ¬IsMin a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<GOAL>InfPrime a ↔ ¬IsMax a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<GOAL>SupIrred a ↔ ¬IsMin a
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>a : α<GOAL>InfIrred a ↔ ¬IsMax a
<VAR>α : Type u_1<VAR>Preorder α<VAR>Nonempty α<GOAL>0 ≤ krullDim α
<VAR>α : Type u_1<VAR>Preorder α<VAR>IsEmpty α<GOAL>krullDim α = ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>InfiniteDimensionalOrder α<GOAL>krullDim α = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : StrictMono f<GOAL>krullDim α ≤ krullDim β
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>height α a ≤ height α b
<VAR>α : Type u_1<VAR>Preorder α<VAR>FiniteDimensionalOrder α<GOAL>krullDim α = ↑(LTSeries.longestOf α).length
<VAR>α : Type u_1<VAR>Preorder α<VAR>Unique α<GOAL>krullDim α = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : ∀ ⦃a b : α⦄, f a < f b → a < b<VAR>hf' : Function.Surjective f<GOAL>krullDim β ≤ krullDim α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<GOAL>krullDim α = krullDim β
<VAR>α : Type u_1<VAR>Preorder α<GOAL>krullDim α = ⨆ a, height α a
<VAR>α : Type u_1<VAR>Preorder α<GOAL>krullDim αᵒᵈ = krullDim α
<VAR>α : Type u_1<VAR>HasCompl α<VAR>a : α<GOAL>Heyting.IsRegular a → aᶜᶜ = a
<VAR>α : Type u_1<VAR>HeytingAlgebra α<GOAL>Heyting.IsRegular ⊥
<VAR>α : Type u_1<VAR>HeytingAlgebra α<GOAL>Heyting.IsRegular ⊤
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a b : α<VAR>ha : Heyting.IsRegular a<VAR>hb : Heyting.IsRegular b<GOAL>Heyting.IsRegular (a ⊓ b)
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a b : α<VAR>ha : Heyting.IsRegular a<VAR>hb : Heyting.IsRegular b<GOAL>Heyting.IsRegular (a ⇨ b)
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a : α<GOAL>Heyting.IsRegular aᶜ
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a b : α<VAR>ha : Heyting.IsRegular a<GOAL>Disjoint aᶜ b ↔ b ≤ a
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a b : α<VAR>hb : Heyting.IsRegular b<GOAL>Disjoint a bᶜ ↔ a ≤ b
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a : Heyting.Regular α<GOAL>Heyting.IsRegular ↑a
<VAR>α : Type u_1<VAR>HeytingAlgebra α<GOAL>Function.Injective Heyting.Regular.val
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a b : Heyting.Regular α<GOAL>↑a = ↑b ↔ a = b
<VAR>α : Type u_1<VAR>HeytingAlgebra α<GOAL>↑⊤ = ⊤
<VAR>α : Type u_1<VAR>HeytingAlgebra α<GOAL>↑⊥ = ⊥
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a b : Heyting.Regular α<GOAL>↑(a ⊓ b) = ↑a ⊓ ↑b
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a b : Heyting.Regular α<GOAL>↑(a ⇨ b) = ↑a ⇨ ↑b
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a : Heyting.Regular α<GOAL>↑aᶜ = (↑a)ᶜ
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a b : Heyting.Regular α<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a b : Heyting.Regular α<GOAL>↑a < ↑b ↔ a < b
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a : α<GOAL>↑(Heyting.Regular.toRegular a) = aᶜᶜ
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a : Heyting.Regular α<GOAL>Heyting.Regular.toRegular ↑a = a
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a b : Heyting.Regular α<GOAL>↑(a ⊔ b) = (↑a ⊔ ↑b)ᶜᶜ
<VAR>α : Type u_1<VAR>HeytingAlgebra α<VAR>a b : Heyting.Regular α<GOAL>↑(a \ b) = ↑a ⊓ (↑b)ᶜ
<VAR>α : Type u_1<VAR>BooleanAlgebra α<VAR>a : α<GOAL>Heyting.IsRegular a
<VAR>p : Prop<VAR>Decidable p<GOAL>Heyting.IsRegular p
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>hwf : WellFounded r<GOAL>∃ s, r ≤ s ∧ IsWellOrder α s
<VAR>α : Type u<VAR>Preorder α<VAR>WellFoundedLT α<GOAL>StrictMono ⇑toWellOrderExtension
<VAR>α : Type u_1<VAR>Preorder α<VAR>self : ClosureOperator α<VAR>x : α<GOAL>self.toFun (self.toFun x) = self.toFun x
<VAR>α : Type u_1<VAR>Preorder α<VAR>self : ClosureOperator α<VAR>x : α<GOAL>self.IsClosed x ↔ self.toFun x = x
<VAR>α : Type u_1<VAR>Preorder α<VAR>self : ClosureOperator α<VAR>x : α<GOAL>x ≤ self.toFun x
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>c : ClosureOperator α<VAR>e : α ≃o β<VAR>a : β<GOAL>(c.conjBy e) a = (e.conj ↑c) a
<VAR>α : Type u_4<VAR>Preorder α<VAR>c : ClosureOperator α<GOAL>c.conjBy (OrderIso.refl α) = c
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>γ : Type u_6<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>e₁ : α ≃o β<VAR>e₂ : β ≃o γ<VAR>c : ClosureOperator α<GOAL>c.conjBy (e₁.trans e₂) = (c.conjBy e₁).conjBy e₂
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>∀ (x : α), (ClosureOperator.id α).IsClosed x = True
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>(ClosureOperator.id α) a = a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c₁ c₂ : ClosureOperator α<GOAL>(∀ (x : α), c₁ x = c₂ x) → c₁ = c₂
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>f : α → α<VAR>hf₁ : Monotone f<VAR>hf₂ : ∀ (x : α), x ≤ f x<VAR>hf₃ : ∀ (x : α), f (f x) ≤ f x<VAR>x : α<GOAL>(ClosureOperator.mk' f hf₁ hf₂ hf₃).IsClosed x = (f x = x)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>f : α → α<VAR>hf₁ : Monotone f<VAR>hf₂ : ∀ (x : α), x ≤ f x<VAR>hf₃ : ∀ (x : α), f (f x) ≤ f x<GOAL>∀ (a : α), (ClosureOperator.mk' f hf₁ hf₂ hf₃) a = f a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>f : α → α<VAR>hf : ∀ (x : α), x ≤ f x<VAR>hmin : ∀ ⦃x y : α⦄, x ≤ f y → f x ≤ f y<GOAL>∀ (a : α), (ClosureOperator.mk₂ f hf hmin) a = f a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>f : α → α<VAR>hf : ∀ (x : α), x ≤ f x<VAR>hmin : ∀ ⦃x y : α⦄, x ≤ f y → f x ≤ f y<VAR>x : α<GOAL>(ClosureOperator.mk₂ f hf hmin).IsClosed x = (f x = x)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>f : α → α<VAR>p : α → Prop<VAR>hf : ∀ (x : α), x ≤ f x<VAR>hfp : ∀ (x : α), p (f x)<VAR>hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f x ≤ y<GOAL>∀ (a : α), (ClosureOperator.ofPred f p hf hfp hmin).IsClosed a = p a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>f : α → α<VAR>p : α → Prop<VAR>hf : ∀ (x : α), x ≤ f x<VAR>hfp : ∀ (x : α), p (f x)<VAR>hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f x ≤ y<GOAL>∀ (a : α), (ClosureOperator.ofPred f p hf hfp hmin) a = f a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<GOAL>Monotone ⇑c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<VAR>x : α<GOAL>x ≤ c x
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<VAR>x : α<GOAL>c (c x) = c x
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<VAR>x : α<GOAL>c.IsClosed (c x)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<VAR>x : α<GOAL>c.IsClosed x → c x = x
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<VAR>x : α<GOAL>c.IsClosed x ↔ c x ≤ x
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<GOAL>{x | c.IsClosed x} = Set.range ⇑c
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<VAR>x y : α<GOAL>x ≤ c y ↔ c x ≤ c y
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<VAR>x y : α<VAR>hy : c.IsClosed y<GOAL>c x ≤ y ↔ x ≤ y
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<VAR>x y : α<VAR>hxy : x ≤ y<VAR>hy : c.IsClosed y<GOAL>c x ≤ y
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<VAR>x : α<GOAL>IsGLB {y | x ≤ y ∧ c.IsClosed y} (c x)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c₁ c₂ : ClosureOperator α<VAR>h : ∀ (x : α), c₁.IsClosed x ↔ c₂.IsClosed x<GOAL>c₁ = c₂
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>c : ClosureOperator α<GOAL>c = ClosureOperator.ofPred (⇑c) c.IsClosed ⋯ ⋯ ⋯
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>c : ClosureOperator α<GOAL>c ⊤ = ⊤
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>c : ClosureOperator α<GOAL>c.IsClosed ⊤
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>c : ClosureOperator α<VAR>x y : α<GOAL>c (x ⊓ y) ≤ c x ⊓ c y
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>c : ClosureOperator α<VAR>x y : α<GOAL>c x ⊔ c y ≤ c (x ⊔ y)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>c : ClosureOperator α<VAR>x y : α<GOAL>c (c x ⊔ y) = c (x ⊔ y)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>c : ClosureOperator α<VAR>x y : α<GOAL>c (x ⊔ c y) = c (x ⊔ y)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>c : ClosureOperator α<VAR>x y : α<GOAL>c (c x ⊔ c y) = c (x ⊔ y)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p : α → Prop<VAR>hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)<GOAL>∀ (a : α), (ClosureOperator.ofCompletePred p hsinf).IsClosed a = p a
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>p : α → Prop<VAR>hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)<VAR>a : α<GOAL>(ClosureOperator.ofCompletePred p hsinf) a = ⨅ b, ↑b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>c : ClosureOperator α<VAR>S : Set α<VAR>H : ∀ x ∈ S, c.IsClosed x<GOAL>c.IsClosed (sInf S)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>CompleteLattice α<VAR>c : ClosureOperator α<VAR>f : ι → α<GOAL>c (⨆ i, c (f i)) = c (⨆ i, f i)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>CompleteLattice α<VAR>c : ClosureOperator α<VAR>f : (i : ι) → κ i → α<GOAL>c (⨆ i, ⨆ j, c (f i j)) = c (⨆ i, ⨆ j, f i j)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>c : ClosureOperator α<GOAL>e.equivClosureOperator c = c.conjBy e
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>c : ClosureOperator β<GOAL>e.equivClosureOperator.symm c = c.conjBy e.symm
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>u : β → α<VAR>self : LowerAdjoint u<GOAL>GaloisConnection self.toFun u
<VAR>α : Type u_1<VAR>Preorder α<VAR>x : α<GOAL>(LowerAdjoint.id α).toFun x = x
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<GOAL>GaloisConnection l.toFun u
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>u : β → α<VAR>l₁ l₂ : LowerAdjoint u<GOAL>l₁.toFun = l₂.toFun → l₁ = l₂
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<GOAL>Monotone (u ∘ l.toFun)
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x : α<GOAL>x ≤ u (l.toFun x)
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>PartialOrder α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x : α<GOAL>l.closureOperator.IsClosed x = (u (l.toFun x) = x)
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>PartialOrder α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x : α<GOAL>l.closureOperator x = u (l.toFun x)
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>PartialOrder α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x : α<GOAL>u (l.toFun (u (l.toFun x))) = u (l.toFun x)
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>PartialOrder α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x y : α<GOAL>x ≤ u (l.toFun y) ↔ u (l.toFun x) ≤ u (l.toFun y)
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x : α<GOAL>x ∈ l.closed ↔ u (l.toFun x) = x
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>Preorder α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x : α<VAR>h : x ∈ l.closed<GOAL>u (l.toFun x) = x
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>PartialOrder α<VAR>PartialOrder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x : α<GOAL>x ∈ l.closed ↔ u (l.toFun x) ≤ x
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>PartialOrder α<VAR>PartialOrder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x : α<GOAL>u (l.toFun x) ∈ l.closed
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>PartialOrder α<VAR>PartialOrder β<VAR>u : β → α<VAR>l : LowerAdjoint u<GOAL>l.closed = Set.range (u ∘ l.toFun)
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>PartialOrder α<VAR>PartialOrder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x : α<VAR>y : α<VAR>hy : l.closed y<GOAL>u (l.toFun x) ≤ y ↔ x ≤ y
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>PartialOrder α<VAR>OrderTop α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<GOAL>u (l.toFun ⊤) = ⊤
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SemilatticeInf α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x y : α<GOAL>u (l.toFun (x ⊓ y)) ≤ u (l.toFun x) ⊓ u (l.toFun y)
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x y : α<GOAL>u (l.toFun x) ⊔ u (l.toFun y) ≤ u (l.toFun (x ⊔ y))
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x y : α<GOAL>u (l.toFun (u (l.toFun x) ⊔ y)) = u (l.toFun (x ⊔ y))
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x y : α<GOAL>u (l.toFun (x ⊔ u (l.toFun y))) = u (l.toFun (x ⊔ y))
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SemilatticeSup α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>x y : α<GOAL>u (l.toFun (u (l.toFun x) ⊔ u (l.toFun y))) = u (l.toFun (x ⊔ y))
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Type u_4<VAR>CompleteLattice α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>f : ι → α<GOAL>u (l.toFun (⨆ i, u (l.toFun (f i)))) = u (l.toFun (⨆ i, f i))
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>β : Type u_4<VAR>CompleteLattice α<VAR>Preorder β<VAR>u : β → α<VAR>l : LowerAdjoint u<VAR>f : (i : ι) → κ i → α<GOAL>u (l.toFun (⨆ i, ⨆ j, u (l.toFun (f i j)))) = u (l.toFun (⨆ i, ⨆ j, f i j))
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SetLike α β<VAR>l : LowerAdjoint SetLike.coe<VAR>s : Set β<GOAL>s ⊆ ↑(l.toFun s)
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SetLike α β<VAR>l : LowerAdjoint SetLike.coe<VAR>s : Set β<VAR>P : β<VAR>hP : P ∉ l.toFun s<GOAL>P ∉ s
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SetLike α β<VAR>l : LowerAdjoint SetLike.coe<VAR>s : Set β<VAR>S : α<GOAL>l.toFun s ≤ S ↔ s ⊆ ↑S
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SetLike α β<VAR>l : LowerAdjoint SetLike.coe<VAR>s : Set β<VAR>x : β<GOAL>x ∈ l.toFun s ↔ ∀ (S : α), s ⊆ ↑S → x ∈ S
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SetLike α β<VAR>l : LowerAdjoint SetLike.coe<VAR>s : Set β<VAR>S : α<VAR>h₁ : s ⊆ ↑S<VAR>h₂ : S ≤ l.toFun s<GOAL>l.toFun s = S
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SetLike α β<VAR>l : LowerAdjoint SetLike.coe<VAR>x y : α<GOAL>↑(l.toFun ↑x) ∪ ↑(l.toFun ↑y) ⊆ ↑(l.toFun (↑x ∪ ↑y))
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SetLike α β<VAR>l : LowerAdjoint SetLike.coe<VAR>x y : α<GOAL>l.toFun (↑(l.toFun ↑x) ∪ ↑y) = l.toFun (↑x ∪ ↑y)
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>SetLike α β<VAR>l : LowerAdjoint SetLike.coe<VAR>x y : α<GOAL>l.toFun (↑x ∪ ↑(l.toFun ↑y)) = l.toFun (↑x ∪ ↑y)