ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<GOAL>ComplementedLattice ↥L ↔ ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<VAR>s : Set α<VAR>hs : s = ↑L<GOAL>↑(L.copy s hs) = s
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>L : CompleteSublattice α<VAR>s : Set α<VAR>hs : s = ↑L<GOAL>L.copy s hs = L
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<GOAL>↑f.range = Set.range ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>hf : Function.Injective ⇑f<VAR>a : α<GOAL>(f.toOrderIsoRangeOfInjective hf) a = ⟨f a, ⋯⟩
<VAR>α : Type u_1<VAR>a : α<GOAL>(Booleanisation.lift a)ᶜ = Booleanisation.comp a
<VAR>α : Type u_1<VAR>a : α<GOAL>(Booleanisation.comp a)ᶜ = Booleanisation.lift a
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.lift a ≤ Booleanisation.lift b ↔ a ≤ b
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.comp a ≤ Booleanisation.comp b ↔ b ≤ a
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.lift a ≤ Booleanisation.comp b ↔ Disjoint a b
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>¬Booleanisation.comp a ≤ Booleanisation.lift b
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.lift a < Booleanisation.lift b ↔ a < b
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.comp a < Booleanisation.comp b ↔ b < a
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.lift a < Booleanisation.comp b ↔ Disjoint a b
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>¬Booleanisation.comp a < Booleanisation.lift b
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.lift a ⊔ Booleanisation.lift b = Booleanisation.lift (a ⊔ b)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.lift a ⊔ Booleanisation.comp b = Booleanisation.comp (b \ a)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.comp a ⊔ Booleanisation.lift b = Booleanisation.comp (a \ b)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.comp a ⊔ Booleanisation.comp b = Booleanisation.comp (a ⊓ b)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.lift a ⊓ Booleanisation.lift b = Booleanisation.lift (a ⊓ b)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.lift a ⊓ Booleanisation.comp b = Booleanisation.lift (a \ b)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.comp a ⊓ Booleanisation.lift b = Booleanisation.lift (b \ a)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.comp a ⊓ Booleanisation.comp b = Booleanisation.comp (a ⊔ b)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<GOAL>Booleanisation.lift ⊥ = ⊥
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<GOAL>Booleanisation.comp ⊥ = ⊤
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.lift a \ Booleanisation.lift b = Booleanisation.lift (a \ b)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.lift a \ Booleanisation.comp b = Booleanisation.lift (a ⊓ b)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.comp a \ Booleanisation.lift b = Booleanisation.comp (a ⊔ b)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>Booleanisation.comp a \ Booleanisation.comp b = Booleanisation.lift (b \ a)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<GOAL>Function.Injective ⇑Booleanisation.liftLatticeHom
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>x : (i : ι) → β i<VAR>i : ι<GOAL>toLex x i = x i
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>x : Lex ((i : ι) → β i)<VAR>i : ι<GOAL>ofLex x i = x i
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>(i : ι) → Preorder (β i)<VAR>r : ι → ι → Prop<VAR>hwf : WellFounded r<VAR>x y : (i : ι) → β i<VAR>hlt : x < y<GOAL>∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>(i : ι) → PartialOrder (β i)<VAR>r : ι → ι → Prop<VAR>hwf : WellFounded r<VAR>x y : (i : ι) → β i<VAR>hlt : x < y<GOAL>Pi.Lex r (fun i x x_1 => x < x_1) x y
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>∀ (i : ι), IsTrichotomous (β i) s<VAR>wf : WellFounded r<GOAL>IsTrichotomous ((i : ι) → β i) (Pi.Lex r s)
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>LinearOrder ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>(i : ι) → PartialOrder (β i)<GOAL>Monotone ⇑toLex
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>LinearOrder ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>(i : ι) → PartialOrder (β i)<GOAL>StrictMono ⇑toLex
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>LinearOrder ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>(i : ι) → PartialOrder (β i)<VAR>x : (i : ι) → β i<VAR>i : ι<VAR>a : β i<GOAL>toLex x < toLex (Function.update x i a) ↔ x i < a
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>LinearOrder ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>(i : ι) → PartialOrder (β i)<VAR>x : (i : ι) → β i<VAR>i : ι<VAR>a : β i<GOAL>toLex (Function.update x i a) < toLex x ↔ a < x i
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>LinearOrder ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>(i : ι) → PartialOrder (β i)<VAR>x : (i : ι) → β i<VAR>i : ι<VAR>a : β i<GOAL>toLex x ≤ toLex (Function.update x i a) ↔ x i ≤ a
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>LinearOrder ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>(i : ι) → PartialOrder (β i)<VAR>x : (i : ι) → β i<VAR>i : ι<VAR>a : β i<GOAL>toLex (Function.update x i a) ≤ toLex x ↔ a ≤ x i
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>Preorder ι<VAR>(i : ι) → LT (β i)<VAR>i : ι<VAR>NoMaxOrder (β i)<GOAL>NoMaxOrder (Lex ((i : ι) → β i))
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>Preorder ι<VAR>DecidableEq ι<VAR>Preorder α<VAR>f : ι → α<VAR>i j : ι<VAR>h₁ : i ≤ j<VAR>h₂ : f j < f i<GOAL>toLex (f ∘ ⇑(Equiv.swap i j)) < toLex f
<VAR>α : Type u_1<VAR>Preorder α<VAR>Nonempty α<VAR>NoMaxOrder α<GOAL>Infinite α
<VAR>α : Type u_1<VAR>Preorder α<VAR>Nonempty α<VAR>NoMinOrder α<GOAL>Infinite α
<VAR>α : Type u_1<VAR>Preorder α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>Infinite ↑(Set.Ioo a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>(Set.Ioo a b).Infinite
<VAR>α : Type u_1<VAR>Preorder α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>(Set.Ico a b).Infinite
<VAR>α : Type u_1<VAR>Preorder α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>Infinite ↑(Set.Ico a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>(Set.Ioc a b).Infinite
<VAR>α : Type u_1<VAR>Preorder α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>Infinite ↑(Set.Ioc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>(Set.Icc a b).Infinite
<VAR>α : Type u_1<VAR>Preorder α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>Infinite ↑(Set.Icc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMinOrder α<VAR>a : α<GOAL>(Set.Iio a).Infinite
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMinOrder α<VAR>a : α<GOAL>(Set.Iic a).Infinite
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>(Set.Ioi a).Infinite
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>(Set.Ici a).Infinite
<VAR>α : Type u_2<VAR>s : Set α<VAR>Preorder α<VAR>SupSet α<VAR>Inhabited ↑s<GOAL>sSup = fun t => if ht : t.Nonempty ∧ BddAbove t ∧ sSup (Subtype.val '' t) ∈ s then ⟨sSup (Subtype.val '' t), ⋯⟩ else default
<VAR>α : Type u_2<VAR>s : Set α<VAR>Preorder α<VAR>SupSet α<VAR>Inhabited ↑s<VAR>t : Set ↑s<VAR>h' : t.Nonempty<VAR>h'' : BddAbove t<VAR>h : sSup (Subtype.val '' t) ∈ s<GOAL>sSup (Subtype.val '' t) = ↑(sSup t)
<VAR>α : Type u_2<VAR>s : Set α<VAR>Preorder α<VAR>SupSet α<VAR>Inhabited ↑s<GOAL>sSup ∅ = default
<VAR>α : Type u_2<VAR>s : Set α<VAR>Preorder α<VAR>SupSet α<VAR>Inhabited ↑s<VAR>t : Set ↑s<VAR>ht : ¬BddAbove t<GOAL>sSup t = default
<VAR>α : Type u_2<VAR>s : Set α<VAR>Preorder α<VAR>InfSet α<VAR>Inhabited ↑s<GOAL>sInf = fun t => if ht : t.Nonempty ∧ BddBelow t ∧ sInf (Subtype.val '' t) ∈ s then ⟨sInf (Subtype.val '' t), ⋯⟩ else default
<VAR>α : Type u_2<VAR>s : Set α<VAR>Preorder α<VAR>InfSet α<VAR>Inhabited ↑s<VAR>t : Set ↑s<VAR>h' : t.Nonempty<VAR>h'' : BddBelow t<VAR>h : sInf (Subtype.val '' t) ∈ s<GOAL>sInf (Subtype.val '' t) = ↑(sInf t)
<VAR>α : Type u_2<VAR>s : Set α<VAR>Preorder α<VAR>InfSet α<VAR>Inhabited ↑s<GOAL>sInf ∅ = default
<VAR>α : Type u_2<VAR>s : Set α<VAR>Preorder α<VAR>InfSet α<VAR>Inhabited ↑s<VAR>t : Set ↑s<VAR>ht : ¬BddBelow t<GOAL>sInf t = default
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>t : Set ↑s<VAR>ht : t.Nonempty<VAR>h_bdd : BddAbove t<GOAL>sSup (Subtype.val '' t) ∈ s
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hs : s.OrdConnected<VAR>t : Set ↑s<VAR>ht : t.Nonempty<VAR>h_bdd : BddBelow t<GOAL>sInf (Subtype.val '' t) ∈ s
<VAR>α : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>a b : α<VAR>h : a ≤ b<VAR>S : Set ↑(Set.Icc a b)<VAR>hS : S.Nonempty<GOAL>↑(sSup S) = sSup (Subtype.val '' S)
<VAR>α : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>a b : α<VAR>h : a ≤ b<VAR>S : Set ↑(Set.Icc a b)<VAR>hS : S.Nonempty<GOAL>↑(sInf S) = sInf (Subtype.val '' S)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>a b : α<VAR>h : a ≤ b<VAR>Nonempty ι<VAR>S : ι → ↑(Set.Icc a b)<GOAL>↑(iSup S) = ⨆ i, ↑(S i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLattice α<VAR>a b : α<VAR>h : a ≤ b<VAR>Nonempty ι<VAR>S : ι → ↑(Set.Icc a b)<GOAL>↑(iInf S) = ⨅ i, ↑(S i)
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>a : α<VAR>S : Set ↑(Set.Iic a)<GOAL>↑(sSup S) = sSup (Subtype.val '' S)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>a : α<VAR>f : ι → ↑(Set.Iic a)<GOAL>↑(⨆ i, f i) = ⨆ i, ↑(f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>a : α<VAR>f : ι → ↑(Set.Iic a)<VAR>p : ι → Prop<GOAL>↑(⨆ i, ⨆ (_ : p i), f i) = ⨆ i, ⨆ (_ : p i), ↑(f i)
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>a : α<VAR>S : Set ↑(Set.Iic a)<GOAL>↑(sInf S) = a ⊓ sInf (Subtype.val '' S)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>a : α<VAR>f : ι → ↑(Set.Iic a)<GOAL>↑(⨅ i, f i) = a ⊓ ⨅ i, ↑(f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>a : α<VAR>f : ι → ↑(Set.Iic a)<VAR>p : ι → Prop<GOAL>↑(⨅ i, ⨅ (_ : p i), f i) = a ⊓ ⨅ i, ⨅ (_ : p i), ↑(f i)
<VAR>α : Type u<VAR>CompleteLattice α<VAR>k : α<GOAL>CompleteLattice.IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>k : α<GOAL>CompleteLattice.IsCompactElement k ↔ ∀ (s : Set α), s.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>k : α<VAR>hk : CompleteLattice.IsCompactElement k<VAR>ι : Type u_3<VAR>f : ι → α<VAR>h : k ≤ ⨆ i, f i<GOAL>∃ s, k ≤ ⨆ i ∈ s, f i
<VAR>α : Type u_3<VAR>CompleteLattice α<VAR>k : α<VAR>hk : CompleteLattice.IsCompactElement k<VAR>s : Set α<VAR>hemp : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hbelow : ∀ x ∈ s, x < k<GOAL>sSup s < k
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>CompleteLattice α<VAR>f : β → α<VAR>s : Finset β<VAR>h : ∀ x ∈ s, CompleteLattice.IsCompactElement (f x)<GOAL>CompleteLattice.IsCompactElement (s.sup f)
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>h : WellFounded fun x x_1 => x > x_1<GOAL>CompleteLattice.IsSupFiniteCompact α
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>h : CompleteLattice.IsSupFiniteCompact α<GOAL>CompleteLattice.IsSupClosedCompact α
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>h : CompleteLattice.IsSupClosedCompact α<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>α : Type u_2<VAR>CompleteLattice α<GOAL>CompleteLattice.IsSupFiniteCompact α ↔ ∀ (k : α), CompleteLattice.IsCompactElement k
<VAR>α : Type u_2<VAR>CompleteLattice α<GOAL>[WellFounded fun x x_1 => x > x_1, CompleteLattice.IsSupFiniteCompact α, CompleteLattice.IsSupClosedCompact α, ∀ (k : α), CompleteLattice.IsCompactElement k].TFAE
<VAR>α : Type u_2<VAR>CompleteLattice α<GOAL>(WellFounded fun x x_1 => x > x_1) ↔ CompleteLattice.IsSupFiniteCompact α
<VAR>α : Type u_2<VAR>CompleteLattice α<GOAL>CompleteLattice.IsSupFiniteCompact α ↔ CompleteLattice.IsSupClosedCompact α
<VAR>α : Type u_2<VAR>CompleteLattice α<GOAL>CompleteLattice.IsSupClosedCompact α ↔ WellFounded fun x x_1 => x > x_1
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>h : WellFounded fun x x_1 => x > x_1<VAR>s : Set α<VAR>hs : CompleteLattice.SetIndependent s<GOAL>s.Finite
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>hwf : WellFounded fun x x_1 => x > x_1<VAR>ι : Type u_3<VAR>t : ι → α<VAR>ht : CompleteLattice.Independent t<GOAL>{i | t i ≠ ⊥}.Finite
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>hwf : WellFounded fun x x_1 => x > x_1<VAR>ι : Type u_3<VAR>t : ι → α<VAR>ht : CompleteLattice.Independent t<VAR>h_ne_bot : ∀ (i : ι), t i ≠ ⊥<GOAL>Finite ι
<VAR>α : Type u_3<VAR>CompleteLattice α<VAR>self : IsCompactlyGenerated α<VAR>x : α<GOAL>∃ s, (∀ x ∈ s, CompleteLattice.IsCompactElement x) ∧ sSup s = x
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>b : α<GOAL>sSup {c | CompleteLattice.IsCompactElement c ∧ c ≤ b} = b
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<GOAL>sSup {a | CompleteLattice.IsCompactElement a} = ⊤
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>a b : α<GOAL>a ≤ b ↔ ∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a → c ≤ b
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>a : α<VAR>s : Set α<VAR>h : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>a : α<VAR>s : Set α<VAR>h : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>f : ι → α<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>a : α<VAR>h : Directed (fun x x_1 => x ≤ x_1) f<GOAL>a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>f : ι → α<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>a : α<VAR>h : Directed (fun x x_1 => x ≤ x_1) f<GOAL>(⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>a : α<VAR>s : Set α<VAR>h : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>Disjoint a (sSup s) ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint a b
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>a : α<VAR>s : Set α<VAR>h : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>Disjoint (sSup s) a ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint b a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>f : ι → α<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>a : α<VAR>h : Directed (fun x x_1 => x ≤ x_1) f<GOAL>Disjoint a (⨆ i, f i) ↔ ∀ (i : ι), Disjoint a (f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>f : ι → α<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>a : α<VAR>h : Directed (fun x x_1 => x ≤ x_1) f<GOAL>Disjoint (⨆ i, f i) a ↔ ∀ (i : ι), Disjoint (f i) a
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>a : α<VAR>s : Set α<GOAL>a ⊓ sSup s = ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>s : Set α<GOAL>CompleteLattice.SetIndependent s ↔ ∀ (t : Finset α), ↑t ⊆ s → CompleteLattice.SetIndependent ↑t
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>ι : Type u_3<VAR>f : ι → α<VAR>hf : Set.InjOn f {i | f i ≠ ⊥}<GOAL>CompleteLattice.Independent f ↔ ∀ (s : Finset ι), s.SupIndep f
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>η : Type u_3<VAR>s : η → Set α<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ (i : η), CompleteLattice.SetIndependent (s i)<GOAL>CompleteLattice.SetIndependent (⋃ i, s i)
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>s : Set (Set α)<VAR>hs : DirectedOn (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, CompleteLattice.SetIndependent a<GOAL>CompleteLattice.SetIndependent (⋃₀ s)
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>h : WellFounded fun x x_1 => x > x_1<GOAL>IsCompactlyGenerated α
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>k : α<VAR>h : CompleteLattice.IsCompactElement k<GOAL>IsCoatomic ↑(Set.Iic k)
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>h : CompleteLattice.IsCompactElement ⊤<GOAL>IsCoatomic α
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsModularLattice α<VAR>IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<VAR>b : α<GOAL>∃ s, CompleteLattice.SetIndependent s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsModularLattice α<VAR>IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<GOAL>∃ s, CompleteLattice.SetIndependent s ∧ sSup s = ⊤ ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsModularLattice α<VAR>IsCompactlyGenerated α<VAR>h : sSup {a | IsAtom a} = ⊤<GOAL>ComplementedLattice α
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsModularLattice α<VAR>IsCompactlyGenerated α<VAR>IsAtomistic α<GOAL>ComplementedLattice α
<VAR>α : Type u_2<VAR>CompleteLattice α<VAR>IsModularLattice α<VAR>IsCompactlyGenerated α<GOAL>ComplementedLattice α ↔ IsAtomistic α
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x y : α<GOAL>y ∈ s.ordConnectedComponent x ↔ [[x, y]] ⊆ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x : α<GOAL>(⇑OrderDual.ofDual ⁻¹' s).ordConnectedComponent (OrderDual.toDual x) = ⇑OrderDual.ofDual ⁻¹' s.ordConnectedComponent x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x : α<GOAL>s.ordConnectedComponent x ⊆ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x : α<VAR>t : Set α<VAR>h : s.OrdConnected<VAR>hs : x ∈ s<VAR>ht : s ⊆ t<GOAL>s ⊆ t.ordConnectedComponent x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ s.ordConnectedComponent x ↔ x ∈ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x : α<GOAL>(s.ordConnectedComponent x).Nonempty ↔ x ∈ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x : α<GOAL>s.ordConnectedComponent x = ∅ ↔ x ∉ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x : α<GOAL>∅.ordConnectedComponent x = ∅
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>x : α<GOAL>Set.univ.ordConnectedComponent x = Set.univ
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<VAR>x : α<GOAL>(s ∩ t).ordConnectedComponent x = s.ordConnectedComponent x ∩ t.ordConnectedComponent x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x y : α<GOAL>y ∈ s.ordConnectedComponent x ↔ x ∈ s.ordConnectedComponent y
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x y z : α<VAR>hxy : y ∈ s.ordConnectedComponent x<VAR>hyz : z ∈ s.ordConnectedComponent y<GOAL>z ∈ s.ordConnectedComponent x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x y : α<VAR>h : [[x, y]] ⊆ s<GOAL>s.ordConnectedComponent x = s.ordConnectedComponent y
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x : ↑s<GOAL>s.ordConnectedProj x ∈ s.ordConnectedComponent ↑x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x : ↑s<GOAL>↑x ∈ s.ordConnectedComponent (s.ordConnectedProj x)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x : ↑s<GOAL>s.ordConnectedComponent (s.ordConnectedProj x) = s.ordConnectedComponent ↑x
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x y : ↑s<GOAL>s.ordConnectedProj x = s.ordConnectedProj y ↔ [[↑x, ↑y]] ⊆ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<GOAL>(⇑OrderDual.ofDual ⁻¹' s).ordConnectedSection = ⇑OrderDual.ofDual ⁻¹' s.ordConnectedSection
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<GOAL>s.ordConnectedSection ⊆ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<VAR>x y : α<VAR>hx : x ∈ s.ordConnectedSection<VAR>hy : y ∈ s.ordConnectedSection<VAR>h : [[x, y]] ⊆ s<GOAL>x = y
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<GOAL>s.ordSeparatingSet t = t.ordSeparatingSet s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<GOAL>Disjoint s (s.ordSeparatingSet t)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<GOAL>Disjoint t (s.ordSeparatingSet t)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<GOAL>(⇑OrderDual.ofDual ⁻¹' s).ordSeparatingSet (⇑OrderDual.ofDual ⁻¹' t) = ⇑OrderDual.ofDual ⁻¹' s.ordSeparatingSet t
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s t : Set α<GOAL>Disjoint (s.ordT5Nhd t) (t.ordT5Nhd s)
<VAR>α : Type u_2<VAR>Sup α<VAR>SDiff α<VAR>a b : α<GOAL>a ∆ b = a \ b ⊔ b \ a
<VAR>α : Type u_2<VAR>Inf α<VAR>HImp α<VAR>a b : α<GOAL>a ⇔ b = (b ⇨ a) ⊓ (a ⇨ b)
<VAR>p q : Prop<GOAL>p ∆ q = Xor' p q
<VAR>p q : Prop<GOAL>p ⇔ q ↔ (p ↔ q)
<VAR>p q : Bool<GOAL>p ∆ q = xor p q
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>OrderDual.toDual (a ∆ b) = OrderDual.toDual a ⇔ OrderDual.toDual b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual (a ⇔ b) = OrderDual.ofDual a ∆ OrderDual.ofDual b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ∆ b = b ∆ a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a : α<GOAL>a ∆ a = ⊥
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a : α<GOAL>a ∆ ⊥ = a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a : α<GOAL>⊥ ∆ a = a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ∆ b = ⊥ ↔ a = b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<VAR>h : a ≤ b<GOAL>a ∆ b = b \ a
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<VAR>h : b ≤ a<GOAL>a ∆ b = a \ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<VAR>ha : a ≤ b ⊔ c<VAR>hb : b ≤ a ⊔ c<GOAL>a ∆ b ≤ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ∆ b ≤ a ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ∆ b = (a ⊔ b) \ (a ⊓ b)
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<VAR>h : Disjoint a b<GOAL>a ∆ b = a ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ∆ b \ (a ⊓ b) = a ∆ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ∆ (b \ a) = a ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>(a \ b) ∆ b = a ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ∆ b ⊔ a ⊓ b = a ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ⊓ b ⊔ a ∆ b = a ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ∆ b ∆ (a ⊓ b) = a ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>(a ⊓ b) ∆ (a ∆ b) = a ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b c : α<GOAL>a ∆ c ≤ a ∆ b ⊔ b ∆ c
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>a ≤ a ∆ b ⊔ b
<VAR>α : Type u_2<VAR>GeneralizedCoheytingAlgebra α<VAR>a b : α<GOAL>b ≤ a ∆ b ⊔ a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>OrderDual.toDual (a ⇔ b) = OrderDual.toDual a ∆ OrderDual.toDual b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : αᵒᵈ<GOAL>OrderDual.ofDual (a ∆ b) = OrderDual.ofDual a ⇔ OrderDual.ofDual b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ⇔ b = b ⇔ a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a : α<GOAL>a ⇔ a = ⊤
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a : α<GOAL>a ⇔ ⊤ = a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a : α<GOAL>⊤ ⇔ a = a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ⇔ b = ⊤ ↔ a = b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<VAR>h : a ≤ b<GOAL>a ⇔ b = b ⇨ a
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<VAR>h : b ≤ a<GOAL>a ⇔ b = a ⇨ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<VAR>hb : a ⊓ b ≤ c<VAR>hc : a ⊓ c ≤ b<GOAL>a ≤ b ⇔ c
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b c : α<GOAL>a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
<VAR>α : Type u_2<VAR>GeneralizedHeytingAlgebra α<VAR>a b : α<GOAL>a ⊓ b ≤ a ⇔ b