ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>s : Set α<GOAL>BddBelow (⇑e '' s) ↔ BddBelow s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>s : Set β<GOAL>BddAbove (⇑e ⁻¹' s) ↔ BddAbove s
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>s : Set β<GOAL>BddBelow (⇑e ⁻¹' s) ↔ BddBelow s
<VAR>k : ℕ<VAR>h : 0 < k<GOAL>GaloisConnection (fun n => n * k) fun n => n / k
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>self : GaloisInsertion l u<VAR>a : α<VAR>h : u (l a) ≤ a<GOAL>self.choice a h = l a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>self : GaloisInsertion l u<GOAL>GaloisConnection l u
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>self : GaloisInsertion l u<VAR>x : β<GOAL>x ≤ l (u x)
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>PartialOrder β<VAR>gi : GaloisInsertion l u<VAR>b : β<GOAL>l (u b) = b
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>PartialOrder β<VAR>gi : GaloisInsertion l u<GOAL>Function.LeftInverse l u
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>PartialOrder β<VAR>OrderTop α<VAR>OrderTop β<VAR>gi : GaloisInsertion l u<GOAL>l ⊤ = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>PartialOrder β<VAR>gi : GaloisInsertion l u<GOAL>Function.Surjective l
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>PartialOrder β<VAR>gi : GaloisInsertion l u<GOAL>Function.Injective u
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>gi : GaloisInsertion l u<VAR>a b : β<GOAL>l (u a ⊔ u b) = a ⊔ b
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>ι : Sort x<VAR>f : ι → β<GOAL>l (⨆ i, u (f i)) = ⨆ i, f i
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>ι : Sort x<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → β<GOAL>l (⨆ i, ⨆ (hi : p i), u (f i hi)) = ⨆ i, ⨆ (hi : p i), f i hi
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>s : Set β<GOAL>l (sSup (u '' s)) = sSup s
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>gi : GaloisInsertion l u<VAR>a b : β<GOAL>l (u a ⊓ u b) = a ⊓ b
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>ι : Sort x<VAR>f : ι → β<GOAL>l (⨅ i, u (f i)) = ⨅ i, f i
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>ι : Sort x<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → β<GOAL>l (⨅ i, ⨅ (hi : p i), u (f i hi)) = ⨅ i, ⨅ (hi : p i), f i hi
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>s : Set β<GOAL>l (sInf (u '' s)) = sInf s
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>ι : Sort x<VAR>f : ι → α<VAR>hf : ∀ (i : ι), u (l (f i)) = f i<GOAL>l (⨅ i, f i) = ⨅ i, l (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>ι : Sort x<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi<GOAL>l (⨅ i, ⨅ (hi : p i), f i hi) = ⨅ i, ⨅ (hi : p i), l (f i hi)
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>Preorder β<VAR>gi : GaloisInsertion l u<VAR>a b : β<GOAL>u a ≤ u b ↔ a ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>Preorder β<VAR>gi : GaloisInsertion l u<GOAL>StrictMono u
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>Preorder β<VAR>gi : GaloisInsertion l u<VAR>s : Set β<VAR>a : α<VAR>hs : IsLUB (u '' s) a<GOAL>IsLUB s (l a)
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>Preorder β<VAR>gi : GaloisInsertion l u<VAR>s : Set β<VAR>a : α<VAR>hs : IsGLB (u '' s) a<GOAL>IsGLB s (l a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>self : GaloisCoinsertion l u<VAR>a : β<VAR>h : a ≤ l (u a)<GOAL>self.choice a h = u a
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>self : GaloisCoinsertion l u<GOAL>GaloisConnection l u
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>l : α → β<VAR>u : β → α<VAR>self : GaloisCoinsertion l u<VAR>x : α<GOAL>u (l x) ≤ x
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>PartialOrder α<VAR>Preorder β<VAR>gi : GaloisCoinsertion l u<VAR>a : α<GOAL>u (l a) = a
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>PartialOrder α<VAR>Preorder β<VAR>gi : GaloisCoinsertion l u<GOAL>Function.LeftInverse u l
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>PartialOrder α<VAR>Preorder β<VAR>OrderBot α<VAR>OrderBot β<VAR>gi : GaloisCoinsertion l u<GOAL>u ⊥ = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>PartialOrder α<VAR>Preorder β<VAR>gi : GaloisCoinsertion l u<GOAL>Function.Surjective u
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>PartialOrder α<VAR>Preorder β<VAR>gi : GaloisCoinsertion l u<GOAL>Function.Injective l
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>gi : GaloisCoinsertion l u<VAR>a b : α<GOAL>u (l a ⊓ l b) = a ⊓ b
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisCoinsertion l u<VAR>ι : Sort x<VAR>f : ι → α<GOAL>u (⨅ i, l (f i)) = ⨅ i, f i
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisCoinsertion l u<VAR>s : Set α<GOAL>u (sInf (l '' s)) = sInf s
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>gi : GaloisCoinsertion l u<VAR>a b : α<GOAL>u (l a ⊔ l b) = a ⊔ b
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisCoinsertion l u<VAR>ι : Sort x<VAR>f : ι → α<GOAL>u (⨆ i, l (f i)) = ⨆ i, f i
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisCoinsertion l u<VAR>ι : Sort x<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<GOAL>u (⨆ i, ⨆ (hi : p i), l (f i hi)) = ⨆ i, ⨆ (hi : p i), f i hi
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisCoinsertion l u<VAR>s : Set α<GOAL>u (sSup (l '' s)) = sSup s
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisCoinsertion l u<VAR>ι : Sort x<VAR>f : ι → β<VAR>hf : ∀ (i : ι), l (u (f i)) = f i<GOAL>u (⨆ i, f i) = ⨆ i, u (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>gi : GaloisCoinsertion l u<VAR>ι : Sort x<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → β<VAR>hf : ∀ (i : ι) (hi : p i), l (u (f i hi)) = f i hi<GOAL>u (⨆ i, ⨆ (hi : p i), f i hi) = ⨆ i, ⨆ (hi : p i), u (f i hi)
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>Preorder β<VAR>gi : GaloisCoinsertion l u<VAR>a b : α<GOAL>l a ≤ l b ↔ a ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>Preorder β<VAR>gi : GaloisCoinsertion l u<GOAL>StrictMono l
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>Preorder β<VAR>gi : GaloisCoinsertion l u<VAR>s : Set α<VAR>a : β<VAR>hs : IsGLB (l '' s) a<GOAL>IsGLB s (u a)
<VAR>α : Type u<VAR>β : Type v<VAR>l : α → β<VAR>u : β → α<VAR>Preorder α<VAR>Preorder β<VAR>gi : GaloisCoinsertion l u<VAR>s : Set α<VAR>a : β<VAR>hs : IsLUB (l '' s) a<GOAL>IsLUB s (u a)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<GOAL>disjointed f 0 = f 0
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>disjointed f (n + 1) = f (n + 1) \ (partialSups f) n
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<GOAL>disjointed ≤ id
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<GOAL>disjointed f ≤ f
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<GOAL>Pairwise (Disjoint on disjointed f)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<VAR>p : α → Sort u_3<VAR>hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)<VAR>h₀ : p (f 0)<GOAL>disjointedRec hdiff h₀ = h₀
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<VAR>hf : Monotone f<VAR>n : ℕ<GOAL>disjointed f (n + 1) = f (n + 1) \ f n
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<VAR>hf : Monotone f<VAR>n : ℕ<GOAL>disjointed f (n + 1) ⊔ f n = f (n + 1)
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<GOAL>partialSups (disjointed f) = partialSups f
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>f d : ℕ → α<VAR>hdisj : Pairwise (Disjoint on d)<VAR>hsups : partialSups d = partialSups f<GOAL>d = disjointed f
<VAR>α : Type u_1<VAR>CompleteBooleanAlgebra α<VAR>f : ℕ → α<GOAL>⨆ n, disjointed f n = ⨆ n, f n
<VAR>α : Type u_1<VAR>CompleteBooleanAlgebra α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>disjointed f n = f n ⊓ ⨅ i, ⨅ (_ : i < n), (f i)ᶜ
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<GOAL>disjointed f n ⊆ f n
<VAR>α : Type u_1<VAR>f : ℕ → Set α<GOAL>⋃ n, disjointed f n = ⋃ n, f n
<VAR>α : Type u_1<VAR>f : ℕ → Set α<VAR>n : ℕ<GOAL>disjointed f n = f n ∩ ⋂ i, ⋂ (_ : i < n), (f i)ᶜ
<VAR>α : Type u_1<VAR>s : ℕ → Set α<VAR>H : ∀ (x : α), ∃ n, x ∈ s n<VAR>(x : α) → (n : ℕ) → Decidable (x ∈ s n)<VAR>n : ℕ<GOAL>(fun x => Nat.find ⋯) ⁻¹' {n} = disjointed s n
<VAR>α : Type u_2<VAR>Lattice α<VAR>self : Sublattice α<GOAL>InfClosed self.carrier
<VAR>α : Type u_2<VAR>Lattice α<VAR>self : Sublattice α<GOAL>SupClosed self.carrier
<VAR>α : Type u_2<VAR>Lattice α<VAR>L M : Sublattice α<GOAL>↑L = ↑M ↔ L = M
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<GOAL>SupClosed ↑L
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<GOAL>InfClosed ↑L
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<GOAL>IsSublattice ↑L
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<VAR>a : α<GOAL>a ∈ L.carrier ↔ a ∈ L
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set α<VAR>a : α<VAR>h_sup : SupClosed s<VAR>h_inf : InfClosed s<GOAL>a ∈ { carrier := s, supClosed' := h_sup, infClosed' := h_inf } ↔ a ∈ s
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set α<VAR>h_sup : SupClosed s<VAR>h_inf : InfClosed s<GOAL>↑{ carrier := s, supClosed' := h_sup, infClosed' := h_inf } = s
<VAR>α : Type u_2<VAR>Lattice α<VAR>s t : Set α<VAR>hs_sup : SupClosed s<VAR>hs_inf : InfClosed s<VAR>ht_sup : SupClosed t<VAR>ht_inf : InfClosed t<GOAL>{ carrier := s, supClosed' := hs_sup, infClosed' := hs_inf } ≤ { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } ↔ s ⊆ t
<VAR>α : Type u_2<VAR>Lattice α<VAR>s t : Set α<VAR>hs_sup : SupClosed s<VAR>hs_inf : InfClosed s<VAR>ht_sup : SupClosed t<VAR>ht_inf : InfClosed t<GOAL>{ carrier := s, supClosed' := hs_sup, infClosed' := hs_inf } < { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } ↔ s ⊂ t
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<VAR>s : Set α<VAR>hs : s = ↑L<GOAL>↑(L.copy s hs) = s
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<VAR>s : Set α<VAR>hs : s = ↑L<GOAL>L.copy s hs = L
<VAR>α : Type u_2<VAR>Lattice α<VAR>L M : Sublattice α<GOAL>(∀ (a : α), a ∈ L ↔ a ∈ M) → L = M
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<VAR>a b : ↥L<GOAL>↑(a ⊔ b) = ↑a ⊔ ↑b
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<VAR>a b : ↥L<GOAL>↑(a ⊓ b) = ↑a ⊓ ↑b
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<VAR>a b : α<VAR>ha : a ∈ L<VAR>hb : b ∈ L<GOAL>⟨a, ha⟩ ⊔ ⟨b, hb⟩ = ⟨a ⊔ b, ⋯⟩
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<VAR>a b : α<VAR>ha : a ∈ L<VAR>hb : b ∈ L<GOAL>⟨a, ha⟩ ⊓ ⟨b, hb⟩ = ⟨a ⊓ b, ⋯⟩
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<GOAL>⇑L.subtype = Subtype.val
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<VAR>a : ↥L<GOAL>L.subtype a = ↑a
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<GOAL>Function.Injective ⇑L.subtype
<VAR>α : Type u_2<VAR>Lattice α<VAR>L M : Sublattice α<VAR>h : L ≤ M<GOAL>⇑(Sublattice.inclusion h) = Set.inclusion h
<VAR>α : Type u_2<VAR>Lattice α<VAR>L M : Sublattice α<VAR>h : L ≤ M<VAR>a : ↥L<GOAL>(Sublattice.inclusion h) a = Set.inclusion h a
<VAR>α : Type u_2<VAR>Lattice α<VAR>L M : Sublattice α<VAR>h : L ≤ M<GOAL>Function.Injective ⇑(Sublattice.inclusion h)
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<GOAL>Sublattice.inclusion ⋯ = LatticeHom.id ↥L
<VAR>α : Type u_2<VAR>Lattice α<VAR>L M : Sublattice α<VAR>h : L ≤ M<GOAL>M.subtype.comp (Sublattice.inclusion h) = L.subtype
<VAR>α : Type u_2<VAR>Lattice α<GOAL>↑⊤ = Set.univ
<VAR>α : Type u_2<VAR>Lattice α<GOAL>↑⊥ = ∅
<VAR>α : Type u_2<VAR>Lattice α<VAR>L M : Sublattice α<GOAL>↑(L ⊓ M) = ↑L ∩ ↑M
<VAR>α : Type u_2<VAR>Lattice α<VAR>S : Set (Sublattice α)<GOAL>↑(sInf S) = ⋂ L ∈ S, ↑L
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>Lattice α<VAR>f : ι → Sublattice α<GOAL>↑(⨅ i, f i) = ⋂ i, ↑(f i)
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<GOAL>↑L = Set.univ ↔ L = ⊤
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<GOAL>↑L = ∅ ↔ L = ⊥
<VAR>α : Type u_2<VAR>Lattice α<VAR>a : α<GOAL>a ∉ ⊥
<VAR>α : Type u_2<VAR>Lattice α<VAR>a : α<GOAL>a ∈ ⊤
<VAR>α : Type u_2<VAR>Lattice α<VAR>L M : Sublattice α<VAR>a : α<GOAL>a ∈ L ⊓ M ↔ a ∈ L ∧ a ∈ M
<VAR>α : Type u_2<VAR>Lattice α<VAR>a : α<VAR>S : Set (Sublattice α)<GOAL>a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>Lattice α<VAR>a : α<VAR>f : ι → Sublattice α<GOAL>a ∈ ⨅ i, f i ↔ ∀ (i : ι), a ∈ f i
<VAR>α : Type u_2<VAR>Lattice α<GOAL>Subsingleton (Sublattice α) ↔ IsEmpty α
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>L : Sublattice β<VAR>f : LatticeHom α β<GOAL>↑(Sublattice.comap f L) = ⇑f ⁻¹' ↑L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>a : α<VAR>L : Sublattice β<GOAL>a ∈ Sublattice.comap f L ↔ f a ∈ L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>Monotone (Sublattice.comap f)
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<GOAL>Sublattice.comap (LatticeHom.id α) L = L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>L : Sublattice γ<VAR>g : LatticeHom β γ<VAR>f : LatticeHom α β<GOAL>Sublattice.comap f (Sublattice.comap g L) = Sublattice.comap (g.comp f) L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>L : Sublattice α<GOAL>↑(Sublattice.map f L) = ⇑f '' ↑L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>L : Sublattice α<VAR>f : LatticeHom α β<VAR>b : β<GOAL>b ∈ Sublattice.map f L ↔ ∃ a ∈ L, f a = b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>L : Sublattice α<VAR>f : LatticeHom α β<VAR>a : α<GOAL>a ∈ L → f a ∈ Sublattice.map f L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>L : Sublattice α<VAR>f : LatticeHom α β<VAR>a : ↥L<GOAL>f ↑a ∈ Sublattice.map f L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>Monotone (Sublattice.map f)
<VAR>α : Type u_2<VAR>Lattice α<VAR>L : Sublattice α<GOAL>Sublattice.map (LatticeHom.id α) L = L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>L : Sublattice α<VAR>g : LatticeHom β γ<VAR>f : LatticeHom α β<GOAL>Sublattice.map g (Sublattice.map f L) = Sublattice.map (g.comp f) L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>L : Sublattice α<VAR>f : α ≃o β<VAR>a : β<GOAL>a ∈ Sublattice.map { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } L ↔ f.symm a ∈ L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>L : Sublattice α<VAR>f : LatticeHom α β<VAR>a : α<VAR>hf : Function.Injective ⇑f<GOAL>f a ∈ Sublattice.map f L ↔ a ∈ L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : α ≃o β<VAR>L : Sublattice α<GOAL>Sublattice.map { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } L = Sublattice.comap { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ } L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : β ≃o α<VAR>L : Sublattice α<GOAL>Sublattice.comap { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ } L = Sublattice.map { toFun := ⇑f.symm, map_sup' := ⋯, map_inf' := ⋯ } L
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>L : Sublattice α<VAR>M : Sublattice β<VAR>e : β ≃o α<GOAL>Sublattice.map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L = M ↔ L = Sublattice.map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>L : Sublattice α<VAR>f : LatticeHom α β<VAR>M : Sublattice β<GOAL>Sublattice.map f L ≤ M ↔ L ≤ Sublattice.comap f M
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>GaloisConnection (Sublattice.map f) (Sublattice.comap f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>Sublattice.map f ⊥ = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>L M : Sublattice α<GOAL>Sublattice.map f (L ⊔ M) = Sublattice.map f L ⊔ Sublattice.map f M
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>L : ι → Sublattice α<GOAL>Sublattice.map f (⨆ i, L i) = ⨆ i, Sublattice.map f (L i)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>Sublattice.comap f ⊤ = ⊤
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>L M : Sublattice β<VAR>f : LatticeHom α β<GOAL>Sublattice.comap f (L ⊓ M) = Sublattice.comap f L ⊓ Sublattice.comap f M
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>s : ι → Sublattice β<GOAL>Sublattice.comap f (iInf s) = ⨅ i, Sublattice.comap f (s i)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>L M : Sublattice α<VAR>f : LatticeHom α β<GOAL>Sublattice.map f (L ⊓ M) ≤ Sublattice.map f L ⊓ Sublattice.map f M
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>L M : Sublattice β<VAR>f : LatticeHom α β<GOAL>Sublattice.comap f L ⊔ Sublattice.comap f M ≤ Sublattice.comap f (L ⊔ M)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>L : ι → Sublattice β<GOAL>⨆ i, Sublattice.comap f (L i) ≤ Sublattice.comap f (⨆ i, L i)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>L M : Sublattice α<VAR>f : LatticeHom α β<VAR>hf : Function.Injective ⇑f<GOAL>Sublattice.map f (L ⊓ M) = Sublattice.map f L ⊓ Sublattice.map f M
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>h : Function.Surjective ⇑f<GOAL>Sublattice.map f ⊤ = ⊤
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>c ≤ min a b ↔ c ≤ a ∧ c ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>a ≤ max b c ↔ a ≤ b ∨ a ≤ c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>min a b ≤ c ↔ a ≤ c ∨ b ≤ c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>max a b ≤ c ↔ a ≤ c ∧ b ≤ c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>a < min b c ↔ a < b ∧ a < c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>a < max b c ↔ a < b ∨ a < c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>min a b < c ↔ a < c ∨ b < c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>max a b < c ↔ a < c ∧ b < c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c d : α<GOAL>a ≤ c → b ≤ d → max a b ≤ max c d
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>c : α<VAR>h : a ≤ b<GOAL>max c a ≤ max c b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>c : α<VAR>h : a ≤ b<GOAL>max a c ≤ max b c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c d : α<GOAL>a ≤ c → b ≤ d → min a b ≤ min c d
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>c : α<VAR>h : a ≤ b<GOAL>min c a ≤ min c b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<VAR>c : α<VAR>h : a ≤ b<GOAL>min a c ≤ min b c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>a ≤ b → a ≤ max b c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>a ≤ c → a ≤ max b c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<VAR>h : a < b<GOAL>a < max b c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<VAR>h : a < c<GOAL>a < max b c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>a ≤ c → min a b ≤ c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>b ≤ c → min a b ≤ c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<VAR>h : a < c<GOAL>min a b < c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<VAR>h : b < c<GOAL>min a b < c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>max a (min b c) = min (max a b) (max a c)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>max (min a b) c = min (max a c) (max b c)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>min a (max b c) = max (min a b) (min a c)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>min (max a b) c = max (min a c) (min b c)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>min a b ≤ max a b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>min a b = a ↔ a ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>min a b = b ↔ b ≤ a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>max a b = a ↔ b ≤ a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>max a b = b ↔ a ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>max a b = a ∧ b ≤ a ∨ max a b = b ∧ a < b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>min a b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>max a b = c ↔ a = c ∧ b ≤ a ∨ b = c ∧ a ≤ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>min a c < min b c ↔ a < b ∧ a < c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>min a b < min a c ↔ b < c ∧ b < a
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>max a c < max b c ↔ a < b ∧ c < b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>max a b < max a c ↔ b < c ∧ a < c
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b : α<GOAL>min a b < max a b ↔ a ≠ b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c d : α<VAR>h₁ : a < c<VAR>h₂ : b < d<GOAL>max a b < max c d
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c d : α<VAR>h₁ : a < c<VAR>h₂ : b < d<GOAL>min a b < min c d
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>min (min a b) c = min (min a c) b
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>max a (max b c) = max b (max a c)
<VAR>α : Type u<VAR>LinearOrder α<VAR>a b c : α<GOAL>max (max a b) c = max (max a c) b
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a b : α<VAR>hf : MonotoneOn f s<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>f (max a b) = max (f a) (f b)
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a b : α<VAR>hf : MonotoneOn f s<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>f (min a b) = min (f a) (f b)
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a b : α<VAR>hf : AntitoneOn f s<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>f (max a b) = min (f a) (f b)
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a b : α<VAR>hf : AntitoneOn f s<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>f (min a b) = max (f a) (f b)
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>a b : α<VAR>hf : Monotone f<GOAL>f (max a b) = max (f a) (f b)
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder α<VAR>LinearOrder β<VAR>f : α → β<VAR>a b : α<VAR>hf : Monotone f<GOAL>f (min a b) = min (f a) (f b)