Loogle!

Result

Found 773 declarations mentioning InfSet.sInf. Of these, only the first 200 are shown.

• InfSet.sInf 📋 Mathlib.Order.SetNotation
  {α : Type u_1} [self : InfSet α] : Set α → α
• Set.sInf_eq_sInter 📋 Mathlib.Order.SetNotation
  {α : Type u} (S : Set (Set α)) : sInf S = ⋂₀ S
• completeLatticeOfInf 📋 Mathlib.Order.CompleteLattice.Defs
  (α : Type u_4) [H1 : PartialOrder α] [H2 : InfSet α] (isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)) : CompleteLattice α
• isGLB_sInf 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] (s : Set α) : IsGLB s (sInf s)
• CompleteSemilatticeInf.isGLB_sInf 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_4} [self : CompleteSemilatticeInf α] (s : Set α) : IsGLB s (sInf s)
• CompleteSemilatticeInf.mk 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_4} [toPartialOrder : PartialOrder α] [toInfSet : InfSet α] (isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)) : CompleteSemilatticeInf α
• CompleteLattice.isGLB_sInf 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_4} [self : CompleteLattice α] (s : Set α) : IsGLB s (sInf s)
• IsGLB.sInf_eq 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : IsGLB s a → sInf s = a
• isGLB_iff_sInf_eq 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : IsGLB s a ↔ sInf s = a
• sInf_mem_lowerBounds 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} : sInf s ∈ lowerBounds s
• sInf_le 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} (h : a ∈ s) : sInf s ≤ a
• sInf_le_sInf 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s t : Set α} (h : s ⊆ t) : sInf t ≤ sInf s
• le_sInf 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} (h : ∀ b ∈ s, a ≤ b) : a ≤ sInf s
• sInf_le_of_le 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a b : α} (hb : b ∈ s) (h : b ≤ a) : sInf s ≤ a
• le_sInf_iff 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b
• sInf_le_iff 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a
• lt_sInf_iff 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {l : α} : l < sInf s ↔ ∃ b, l < b ∧ b ∈ lowerBounds s
• CompleteLattice.mk 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_4} [toLattice : Lattice α] [toSupSet : SupSet α] (isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)) [toInfSet : InfSet α] (isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)) [toBoundedOrder : BoundedOrder α] : CompleteLattice α
• sInf_lt_iff 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteLinearOrder α] {s : Set α} {b : α} : sInf s < b ↔ ∃ a ∈ s, a < b
• ofDual_sInf 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [SupSet α] (s : Set αᵒᵈ) : OrderDual.ofDual (sInf s) = sSup (⇑OrderDual.toDual ⁻¹' s)
• ofDual_sSup 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [InfSet α] (s : Set αᵒᵈ) : OrderDual.ofDual (sSup s) = sInf (⇑OrderDual.toDual ⁻¹' s)
• toDual_sInf 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [InfSet α] (s : Set α) : OrderDual.toDual (sInf s) = sSup (⇑OrderDual.ofDual ⁻¹' s)
• toDual_sSup 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [SupSet α] (s : Set α) : OrderDual.toDual (sSup s) = sInf (⇑OrderDual.ofDual ⁻¹' s)
• sInf_le_iff_forall_lt 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteLinearOrder α] {s : Set α} {l : α} : sInf s ≤ l ↔ ∀ (b : α), l < b → ∃ a ∈ s, a < b
• Equiv.infSet_def 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} {β : Type u_2} (e : α ≃ β) [InfSet β] (s : Set α) : sInf s = e.symm (⨅ a ∈ s, e a)
• sInf_eq_bot 📋 Mathlib.Order.CompleteLattice.Defs
  {α : Type u_1} [CompleteLinearOrder α] {s : Set α} : sInf s = ⊥ ↔ ∀ (b : α), ⊥ < b → ∃ a ∈ s, a < b
• sInf_singleton 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteSemilatticeInf α] {a : α} : sInf {a} = a
• sInf_range 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {ι : Sort u_4} [InfSet α] {f : ι → α} : sInf (Set.range f) = iInf f
• sInf_Prop_eq 📋 Mathlib.Order.CompleteLattice.Basic
  {s : Set Prop} : sInf s = ∀ p ∈ s, p
• iInf_of_isEmpty 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_8} {ι : Sort u_9} [InfSet α] [IsEmpty ι] (f : ι → α) : iInf f = sInf ∅
• sInf_eq_iInf' 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [InfSet α] (s : Set α) : sInf s = ⨅ a, ↑a
• sInf_upperBounds_eq_sSup 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] (s : Set α) : sInf (upperBounds s) = sSup s
• sSup_lowerBounds_eq_sInf 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] (s : Set α) : sSup (lowerBounds s) = sInf s
• sInf_le_sSup 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] {s : Set α} (hs : s.Nonempty) : sInf s ≤ sSup s
• unary_relation_sInf_iff 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_8} (s : Set (α → Prop)) {a : α} : sInf s a ↔ ∀ r ∈ s, r a
• Prod.fst_sInf 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).1 = sInf (Prod.fst '' s)
• Prod.snd_sInf 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).2 = sInf (Prod.snd '' s)
• sInf_le_sInf_of_isCoinitialFor 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteSemilatticeInf α] {s t : Set α} (h : IsCoinitialFor s t) : sInf t ≤ sInf s
• sInf_pair 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] {a b : α} : sInf {a, b} = a ⊓ b
• sInf_image' 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [InfSet α] {s : Set β} {f : β → α} : sInf (f '' s) = ⨅ a, f ↑a
• sInf_apply_eq_sInf_image 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_8} {β : α → Type u_9} [(i : α) → InfSet (β i)] {s : Set ((a : α) → β a)} {a : α} : sInf s a = sInf (Function.eval a '' s)
• sInf_insert 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : sInf (insert a s) = a ⊓ sInf s
• sInf_le_sSup_of_nonempty_inter 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] {s t : Set α} (h : (s ∩ t).Nonempty) : sInf s ≤ sSup t
• sInf_univ 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] : sInf Set.univ = ⊥
• Prod.swap_sInf 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) : (sInf s).swap = sInf (Prod.swap '' s)
• sInf_empty 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] : sInf ∅ = ⊤
• sInf_eq_iInf 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] {s : Set α} : sInf s = ⨅ a ∈ s, a
• sInf_union 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] {s t : Set α} : sInf (s ∪ t) = sInf s ⊓ sInf t
• binary_relation_sInf_iff 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_8} {β : Type u_9} (s : Set (α → β → Prop)) {a : α} {b : β} : sInf s a b ↔ ∀ r ∈ s, r a b
• sInf_prod 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) : sInf (s ×ˢ t) = (sInf s, sInf t)
• sInf_image 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : β → α} : sInf (f '' s) = ⨅ a ∈ s, f a
• le_sInf_inter 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] {s t : Set α} : sInf s ⊔ sInf t ≤ sInf (s ∩ t)
• Antitone.sInf 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (α → β)} (hs : ∀ f ∈ s, Antitone f) : Antitone (sInf s)
• Monotone.sInf 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (α → β)} (hs : ∀ f ∈ s, Monotone f) : Monotone (sInf s)
• sInf_apply 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_8} {β : α → Type u_9} [(i : α) → InfSet (β i)] {s : Set ((a : α) → β a)} {a : α} : sInf s a = ⨅ f, ↑f a
• sInf_sdiff_singleton_top 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] (s : Set α) : sInf (s \ {⊤}) = sInf s
• sInf_eq_of_forall_ge_of_forall_gt_exists_lt 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] {s : Set α} {b : α} (h₁ : ∀ a ∈ s, b ≤ a) (h₂ : ∀ (w : α), b < w → ∃ a ∈ s, a < w) : sInf s = b
• sInf_le_sInf_of_subset_insert_top 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] {s t : Set α} (h : s ⊆ insert ⊤ t) : sInf t ≤ sInf s
• Antitone.le_map_sInf 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : α → β} (hf : Antitone f) : ⨆ a ∈ s, f a ≤ f (sInf s)
• Monotone.map_sInf_le 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) : f (sInf s) ≤ ⨅ a ∈ s, f a
• eq_singleton_top_of_sInf_eq_top_of_nonempty 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] {s : Set α} (h_inf : sInf s = ⊤) (hne : s.Nonempty) : s = {⊤}
• sInf_eq_top 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] {s : Set α} : sInf s = ⊤ ↔ ∀ a ∈ s, a = ⊤
• sInf_image2 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ} : sInf (Set.image2 f s t) = ⨅ a ∈ s, ⨅ b ∈ t, f a b
• sInf_eq_top' 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} [CompleteLattice α] {s : Set α} : sInf s = ⊤ ↔ s = ∅ ∨ s = {⊤}
• OrderIso.map_sInf_eq_sInf_symm_preimage 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (s : Set α) : f (sInf s) = sInf (⇑f.symm ⁻¹' s)
• OrderIso.map_sInf 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (s : Set α) : f (sInf s) = ⨅ a ∈ s, f a
• Function.Injective.completeLattice 📋 Mathlib.Order.CompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [Max α] [Min α] [LE α] [LT α] [SupSet α] [InfSet α] [Top α] [Bot α] [CompleteLattice β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) : CompleteLattice α
• ULift.down_sInf 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [InfSet α] (s : Set (ULift.{v, u_1} α)) : (sInf s).down = sInf (ULift.up ⁻¹' s)
• ULift.up_sInf 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [InfSet α] (s : Set α) : { down := sInf s } = sInf (ULift.down ⁻¹' s)
• codisjoint_sInf_left 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [CompleteLattice α] {a : Set α} {b : α} (d : Codisjoint (sInf a) b) {i : α} (hi : i ∈ a) : Codisjoint i b
• codisjoint_sInf_right 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [CompleteLattice α] {a : Set α} {b : α} (d : Codisjoint b (sInf a)) {i : α} (hi : i ∈ a) : Codisjoint b i
• sInf_sup_le_iInf_sup 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : sInf s ⊔ a ≤ ⨅ b ∈ s, b ⊔ a
• sup_sInf_le_iInf_sup 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} : a ⊔ sInf s ≤ ⨅ b ∈ s, a ⊔ b
• codisjoint_of_sInf_codisjoint 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [CompleteLattice α] {a b : Set α} (hd : Codisjoint (sInf a) (sInf b)) (he : ⊤ ∉ a ∨ ⊤ ∉ b) : Disjoint a b
• GaloisCoinsertion.u_sInf_l_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {u : α → β} {l : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) (s : Set β) : u (sInf (l '' s)) = sInf s
• GaloisConnection.u_sInf_eq_sInf_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {s : Set α} : u (sInf s) = sInf (u '' s)
• GaloisInsertion.l_sInf_u_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {l : α → β} {u : β → α} [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) (s : Set β) : l (sInf (u '' s)) = sInf s
• GaloisConnection.u_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {s : Set α} : u (sInf s) = ⨅ a ∈ s, u a
• sInf_image2_eq_sInf_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (u₂ a) (u a)) : sInf (Set.image2 u s t) = u (sInf s) (sInf t)
• gc_Ici_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} [CompleteSemilatticeInf α] : GaloisConnection (⇑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ⇑OrderDual.ofDual)
• gciIciSInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} [CompleteSemilatticeInf α] : GaloisCoinsertion (⇑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ⇑OrderDual.ofDual)
• gci_Ici_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} [CompleteSemilatticeInf α] : GaloisCoinsertion (⇑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ⇑OrderDual.ofDual)
• sInf_image2_eq_sInf_sSup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) : sInf (Set.image2 u s t) = u (sInf s) (sSup t)
• sInf_image2_eq_sSup_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (u₂ a) (u a)) : sInf (Set.image2 u s t) = u (sSup s) (sInf t)
• sSup_image2_eq_sInf_sSup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) : sSup (Set.image2 l s t) = l (sInf s) (sSup t)
• sSup_image2_eq_sSup_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) : sSup (Set.image2 l s t) = l (sSup s) (sInf t)
• sInf_image2_eq_sSup_sSup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) : sInf (Set.image2 u s t) = u (sSup s) (sSup t)
• sSup_image2_eq_sInf_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) : sSup (Set.image2 l s t) = l (sInf s) (sInf t)
• PUnit.sInf_eq 📋 Mathlib.Order.CompleteBooleanAlgebra
  (s : Set PUnit.{u + 1}) : sInf s = PUnit.unit
• hnot_eq_sInf_codisjoint 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [Order.Coframe α] {a : α} : ￢a = sInf {w | Codisjoint a w}
• compl_sInf' 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [CompleteBooleanAlgebra α] {s : Set α} : (sInf s)ᶜ = sSup (compl '' s)
• compl_sSup' 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [CompleteBooleanAlgebra α] {s : Set α} : (sSup s)ᶜ = sInf (compl '' s)
• codisjoint_sInf_iff 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [Order.Coframe α] {a : α} {s : Set α} : Codisjoint a (sInf s) ↔ ∀ b ∈ s, Codisjoint a b
• sInf_codisjoint_iff 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [Order.Coframe α] {a : α} {s : Set α} : Codisjoint (sInf s) a ↔ ∀ b ∈ s, Codisjoint b a
• sdiff_eq_sInf 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [Order.Coframe α] {a b : α} : a \ b = sInf {w | a ≤ b ⊔ w}
• compl_sInf 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [CompleteBooleanAlgebra α] {s : Set α} : (sInf s)ᶜ = ⨆ i ∈ s, iᶜ
• sInf_sup_eq 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [Order.Coframe α] {s : Set α} {b : α} : sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b
• sup_sInf_eq 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [Order.Coframe α] {s : Set α} {a : α} : a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b
• Order.Coframe.MinimalAxioms.iInf_sup_le_sup_sInf 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [CompleteLattice α] (self : Order.Coframe.MinimalAxioms α) (a : α) (s : Set α) : ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
• Order.Coframe.MinimalAxioms.mk 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [CompleteLattice α] (iInf_sup_le_sup_sInf : ∀ (a : α) (s : Set α), ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s) : Order.Coframe.MinimalAxioms α
• Function.Injective.completelyDistribLatticeMinimalAxioms 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (minAx : CompletelyDistribLattice.MinimalAxioms β) (f : α → β) (hf : Function.Injective f) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) : CompletelyDistribLattice.MinimalAxioms α
• Function.coframeMinimalAxioms 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (maxAx : Order.Coframe.MinimalAxioms β) (f : α → β) (le : ∀ {x y : α}, f y ≤ f x ↔ y ≤ x) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) : Order.Coframe.MinimalAxioms α
• Function.Injective.coframeMinimalAxioms 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (maxAx : Order.Coframe.MinimalAxioms β) (f : α → β) (le : ∀ {x y : α}, f y ≤ f x ↔ y ≤ x) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) : Order.Coframe.MinimalAxioms α
• sInf_sup_sInf 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} [Order.Coframe α] {s t : Set α} : sInf s ⊔ sInf t = ⨅ p ∈ s ×ˢ t, p.1 ⊔ p.2
• Function.completeDistribLatticeMinimalAxioms 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (minAx : CompleteDistribLattice.MinimalAxioms β) (f : α → β) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) : CompleteDistribLattice.MinimalAxioms α
• Function.Injective.completeDistribLatticeMinimalAxioms 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (minAx : CompleteDistribLattice.MinimalAxioms β) (f : α → β) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) : CompleteDistribLattice.MinimalAxioms α
• Function.Injective.completeBooleanAlgebra 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [SupSet α] [InfSet α] [Top α] [Bot α] [Compl α] [HImp α] [SDiff α] [CompleteBooleanAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : CompleteBooleanAlgebra α
• Function.Injective.coframe 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [SupSet α] [InfSet α] [Top α] [Bot α] [HNot α] [SDiff α] [Order.Coframe β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_hnot : ∀ (a : α), f (￢a) = ￢f a) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : Order.Coframe α
• Function.Injective.frame 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [SupSet α] [InfSet α] [Top α] [Bot α] [Compl α] [HImp α] [Order.Frame β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) : Order.Frame α
• Function.Injective.completeAtomicBooleanAlgebra 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [SupSet α] [InfSet α] [Top α] [Bot α] [Compl α] [HImp α] [HNot α] [SDiff α] [CompleteAtomicBooleanAlgebra β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) (map_hnot : ∀ (a : α), f (￢a) = ￢f a) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : CompleteAtomicBooleanAlgebra α
• Function.Injective.completeDistribLattice 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [SupSet α] [InfSet α] [Top α] [Bot α] [Compl α] [HImp α] [HNot α] [SDiff α] [CompleteDistribLattice β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) (map_hnot : ∀ (a : α), f (￢a) = ￢f a) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : CompleteDistribLattice α
• Function.Injective.completelyDistribLattice 📋 Mathlib.Order.CompleteBooleanAlgebra
  {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [SupSet α] [InfSet α] [Top α] [Bot α] [Compl α] [HImp α] [HNot α] [SDiff α] [CompletelyDistribLattice β] (f : α → β) (hf : Function.Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) (map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ) (map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b) (map_hnot : ∀ (a : α), f (￢a) = ￢f a) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) : CompletelyDistribLattice α
• conditionallyCompleteLatticeOfLatticeOfsInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Defs
  (α : Type u_2) [H1 : Lattice α] [InfSet α] (isGLB_sInf : ∀ (s : Set α), BddBelow s → s.Nonempty → IsGLB s (sInf s)) : ConditionallyCompleteLattice α
• ConditionallyCompleteLattice.isGLB_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Defs
  {α : Type u_2} [self : ConditionallyCompleteLattice α] (s : Set α) : s.Nonempty → BddBelow s → IsGLB s (sInf s)
• ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow 📋 Mathlib.Order.ConditionallyCompleteLattice.Defs
  {α : Type u_2} [self : ConditionallyCompleteLinearOrder α] (s : Set α) : ¬BddBelow s → sInf s = sInf ∅
• ConditionallyCompleteLattice.mk 📋 Mathlib.Order.ConditionallyCompleteLattice.Defs
  {α : Type u_2} [toLattice : Lattice α] [toSupSet : SupSet α] [toInfSet : InfSet α] (isLUB_csSup : ∀ (s : Set α), s.Nonempty → BddAbove s → IsLUB s (sSup s)) (isGLB_csInf : ∀ (s : Set α), s.Nonempty → BddBelow s → IsGLB s (sInf s)) : ConditionallyCompleteLattice α
• conditionallyCompleteLatticeOfsInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Defs
  (α : Type u_2) [H1 : PartialOrder α] [H2 : InfSet α] (bddAbove_pair : ∀ (a b : α), BddAbove {a, b}) (bddBelow_pair : ∀ (a b : α), BddBelow {a, b}) (isGLB_sInf : ∀ (s : Set α), BddBelow s → s.Nonempty → IsGLB s (sInf s)) : ConditionallyCompleteLattice α
• ConditionallyCompleteLinearOrder.mk 📋 Mathlib.Order.ConditionallyCompleteLattice.Defs
  {α : Type u_2} [toConditionallyCompleteLattice : ConditionallyCompleteLattice α] [toOrd : Ord α] (le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a) (toDecidableLE : DecidableLE α) (toDecidableEq : DecidableEq α) (toDecidableLT : DecidableLT α) (csSup_of_not_bddAbove : ∀ (s : Set α), ¬BddAbove s → sSup s = sSup ∅) (csInf_of_not_bddBelow : ∀ (s : Set α), ¬BddBelow s → sInf s = sInf ∅) (compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b := by compareOfLessAndEq_rfl) : ConditionallyCompleteLinearOrder α
• ConditionallyCompletePartialOrderInf.mk 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Defs
  {α : Type u_3} [toPartialOrder : PartialOrder α] [toInfSet : InfSet α] (isGLB_csInf_of_directed : ∀ (s : Set α), DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)) : ConditionallyCompletePartialOrderInf α
• ConditionallyCompletePartialOrderInf.isGLB_csInf_of_directed 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Defs
  {α : Type u_3} [self : ConditionallyCompletePartialOrderInf α] (s : Set α) : DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)
• DirectedOn.isGLB_csInf 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Defs
  {α : Type u_2} [ConditionallyCompletePartialOrderInf α] {s : Set α} (h_dir : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (h_non : s.Nonempty) (h_bdd : BddBelow s) : IsGLB s (sInf s)
• ConditionallyCompletePartialOrder.mk 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Defs
  {α : Type u_3} [toConditionallyCompletePartialOrderSup : ConditionallyCompletePartialOrderSup α] [toInfSet : InfSet α] (isGLB_csInf_of_directed : ∀ (s : Set α), DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)) : ConditionallyCompletePartialOrder α
• ConditionallyCompletePartialOrder.isGLB_csInf_of_directed 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Defs
  {α : Type u_3} [self : ConditionallyCompletePartialOrder α] (s : Set α) : DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)
• DirectedOn.csInf_le 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Defs
  {α : Type u_2} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (hs : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (h_bdd : BddBelow s) (ha : a ∈ s) : sInf s ≤ a
• DirectedOn.le_csInf 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Defs
  {α : Type u_2} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (hd : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (h_non : s.Nonempty) (ha : ∀ b ∈ s, a ≤ b) : a ≤ sInf s
• csInf_singleton 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderInf α] (a : α) : sInf {a} = a
• csInf_Ici 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_2} [ConditionallyCompletePartialOrderInf α] {a : α} : sInf (Set.Ici a) = a
• IsLeast.csInf_eq 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (H : IsLeast s a) : sInf s = a
• IsLeast.csInf_mem 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (H : IsLeast s a) : sInf s ∈ s
• csInf_Icc 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_2} [ConditionallyCompletePartialOrderInf α] {a b : α} (h : a ≤ b) : sInf (Set.Icc a b) = a
• csInf_Ico 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_2} [ConditionallyCompletePartialOrderInf α] {a b : α} (h : a < b) : sInf (Set.Ico a b) = a
• inf_eq_bot_of_bot_mem 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} [OrderBot α] (h : ⊥ ∈ s) : sInf s = ⊥
• DirectedOn.notMem_of_lt_csInf 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {x : α} {s : Set α} (hd : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (h : x < sInf s) (hs : BddBelow s) : x ∉ s
• DirectedOn.csInf_le_of_le 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a b : α} (hd : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (hs : BddBelow s) (hb : b ∈ s) (h : b ≤ a) : sInf s ≤ a
• DirectedOn.csInf_lt_of_lt 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a b : α} (hd : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (hs : BddBelow s) (ha : a ∈ s) (h : a < b) : sInf s < b
• DirectedOn.le_csInf_iff 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (hd : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (hb : BddBelow s) (hs : s.Nonempty) : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b
• DirectedOn.csInf_le_csInf 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s t : Set α} (hds : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (hdt : DirectedOn (fun x1 x2 => x2 ≤ x1) t) (ht : BddBelow t) (hs : s.Nonempty) (h : s ⊆ t) : sInf t ≤ sInf s
• DirectedOn.csInf_le_iff 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (hd : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (h : BddBelow s) (hs : s.Nonempty) : sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a
• DirectedOn.csInf_eq_of_forall_ge_of_forall_gt_exists_lt 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {b : α} (hd : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (hs : s.Nonempty) (H : ∀ a ∈ s, b ≤ a) (H' : ∀ (w : α), b < w → ∃ a ∈ s, a < w) : sInf s = b
• DirectedOn.csInf_le_csSup 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrder α] {s : Set α} (hdb : DirectedOn (fun x1 x2 => x1 ≥ x2) s) (hda : DirectedOn (fun x1 x2 => x1 ≤ x2) s) (hb : BddBelow s) (ha : BddAbove s) (ne : s.Nonempty) : sInf s ≤ sSup s
• DirectedOn.subset_Icc_csInf_csSup 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Basic
  {α : Type u_1} [ConditionallyCompletePartialOrder α] {s : Set α} (hdb : DirectedOn (fun x1 x2 => x1 ≥ x2) s) (hda : DirectedOn (fun x1 x2 => x1 ≤ x2) s) (hb : BddBelow s) (ha : BddAbove s) : s ⊆ Set.Icc (sInf s) (sSup s)
• WithTop.sInf_empty 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [LE α] [InfSet α] : sInf ∅ = ⊤
• WithTop.sInf_of_not_bddBelow 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [LE α] [InfSet α] {s : Set (WithTop α)} (h : ¬BddBelow s) : sInf s = ⊤
• IsGLB.csInf_eq 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsGLB s a) (ne : s.Nonempty) : sInf s = a
• WithBot.sInf_singleton_bot 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [LE α] [InfSet α] : sInf {⊥} = ⊥
• WithTop.sInf_singleton_top 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [LE α] [InfSet α] : sInf {⊤} = ⊤
• WithBot.sInf_of_not_bddBelow 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [LE α] [InfSet α] {s : Set (WithBot α)} (h : ¬BddBelow (WithBot.some ⁻¹' s)) : sInf s = ⊥
• WithBot.coe_sInf' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [LE α] [InfSet α] {s : Set α} (hs : BddBelow s) : ↑(sInf s) = sInf ((fun a => ↑a) '' s)
• WithBot.sInf_of_bot_mem 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [LE α] [InfSet α] {s : Set (WithBot α)} (h : ⊥ ∈ s) : sInf s = ⊥
• csInf_pair 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] (a b : α) : sInf {a, b} = a ⊓ b
• csInf_mem 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] (hs : s.Nonempty) : sInf s ∈ s
• WithTop.coe_sInf' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [Preorder α] [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) : ↑(sInf s) = sInf ((fun a => ↑a) '' s)
• isGLB_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (hn : s.Nonempty) (hb : BddBelow s := by bddDefault) : IsGLB s (sInf s)
• csInf_univ 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] [OrderBot α] : sInf Set.univ = ⊥
• csInf_le' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a ∈ s) : sInf s ≤ a
• notMem_of_lt_csInf' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {x : α} {s : Set α} (h : x < sInf s) : x ∉ s
• csInf_le 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : BddBelow s) (h₂ : a ∈ s) : sInf s ≤ a
• csInf_eq_univ_of_not_bddBelow 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} (hs : ¬BddBelow s) : sInf s = sInf Set.univ
• isLeast_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] (hs : s.Nonempty) : IsLeast s (sInf s)
• csInf_of_not_bddBelow 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} (hs : ¬BddBelow s) : sInf s = sInf ∅
• WithBot.isGLB_sInf' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {β : Type u_5} [ConditionallyCompleteLattice β] {s : Set (WithBot β)} (hs : s.Nonempty) : IsGLB s (sInf s)
• le_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : s.Nonempty) (h₂ : ∀ b ∈ s, a ≤ b) : a ≤ sInf s
• notMem_of_lt_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {x : α} {s : Set α} (h : x < sInf s) (hs : BddBelow s) : x ∉ s
• sInf_iUnion_Ici 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] (f : ι → α) : sInf (⋃ i, Set.Ici (f i)) = ⨅ i, f i
• csInf_Ioi 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} [NoMaxOrder α] [DenselyOrdered α] : sInf (Set.Ioi a) = a
• ciInf_eq_univ_of_not_bddBelow 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] {f : ι → α} (hf : ¬BddBelow (Set.range f)) : ⨅ i, f i = sInf Set.univ
• csInf_le_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s t : Set α} (ht : BddBelow t) (hs : s.Nonempty) (h : s ⊆ t) : sInf t ≤ sInf s
• csInf_upperBounds_eq_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddAbove s) (hs : s.Nonempty) : sInf (upperBounds s) = sSup s
• csSup_lowerBounds_eq_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddBelow s) (hs : s.Nonempty) : sSup (lowerBounds s) = sInf s
• WithBot.sInf_eq 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [LE α] [InfSet α] {s : Set (WithBot α)} (hs : ⊥ ∉ s) (hs' : BddBelow (WithBot.some ⁻¹' s)) : sInf s = ↑(sInf (WithBot.some ⁻¹' s))
• csInf_Ioc 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α] (h : b < a) : sInf (Set.Ioc b a) = b
• csInf_Ioo 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α] (h : b < a) : sInf (Set.Ioo b a) = b
• sInf_eq_argmin_on 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] (hs : s.Nonempty) : sInf s = Function.argminOn id s hs
• AntitoneOn.sInf_image_Icc 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b) (h' : AntitoneOn f (Set.Icc a b)) : sInf (f '' Set.Icc a b) = f b
• MonotoneOn.sInf_image_Icc 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b) (h' : MonotoneOn f (Set.Icc a b)) : sInf (f '' Set.Icc a b) = f a
• ciInf_of_not_bddBelow 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] {f : ι → α} (hf : ¬BddBelow (Set.range f)) : ⨅ i, f i = sInf ∅
• WithTop.isGLB_sInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] (s : Set (WithTop α)) : IsGLB s (sInf s)
• WithTop.sInf_eq 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [LE α] [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) (h's : BddBelow s) : sInf s = ↑(sInf (WithTop.some ⁻¹' s))
• csInf_insert 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (hs : BddBelow s) (sne : s.Nonempty) : sInf (insert a s) = a ⊓ sInf s
• csInf_le_csInf' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s t : Set α} (h₁ : t.Nonempty) (h₂ : t ⊆ s) : sInf s ≤ sInf t
• csInf_le_of_le 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a b : α} (hs : BddBelow s) (hb : b ∈ s) (h : b ≤ a) : sInf s ≤ a
• csInf_upperBounds_range 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [Nonempty β] {f : β → α} (hf : BddAbove (Set.range f)) : sInf (upperBounds (Set.range f)) = ⨆ i, f i
• exists_lt_of_csInf_lt 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} (hs : s.Nonempty) (hb : sInf s < b) : ∃ a ∈ s, a < b
• WithBot.sInf_empty 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  (α : Type u_5) [CompleteLattice α] : sInf ∅ = ⊤
• WithTop.isGLB_sInf' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {β : Type u_5} [ConditionallyCompleteLattice β] {s : Set (WithTop β)} (hs : BddBelow s) : IsGLB s (sInf s)
• csInf_lt_of_lt 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a b : α} (hs : BddBelow s) (ha : a ∈ s) (h : a < b) : sInf s < b
• Monotone.csInf_image_le 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice β] [Preorder α] {f : α → β} (h_mono : Monotone f) {s : Set α} {c : α} (hcs : c ∈ s) (h_bdd : BddBelow s) : sInf (f '' s) ≤ f c
• le_csInf_iff' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (ne : s.Nonempty) : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b
• le_csInf_iff'' 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (ne : s.Nonempty) : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b
• subset_Icc_csInf_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (hb : BddBelow s) (ha : BddAbove s) : s ⊆ Set.Icc (sInf s) (sSup s)
• Monotone.le_csInf_image 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice β] [Preorder α] {f : α → β} (h_mono : Monotone f) {s : Set α} (hs : s.Nonempty) {B : α} (hB : B ∈ lowerBounds s) : f B ≤ sInf (f '' s)
• le_csInf_iff 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (hb : BddBelow s) (hs : s.Nonempty) : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b
• csInf_le_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (ne : s.Nonempty) (hb : BddBelow s := by bddDefault) (ha : BddAbove s := by bddDefault) : sInf s ≤ sSup s
• csInf_eq_iff 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] (hs : s.Nonempty) (n : α) : sInf s = n ↔ n ∈ s ∧ ∀ a ∈ s, n ≤ a
• le_csInf_union 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] (s t : Set α) : min (sInf s) (sInf t) ≤ sInf (s ∪ t)
• le_csInf_iff_of_wellFoundedLT 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} [WellFoundedLT α] (hs : s.Nonempty) : b ≤ sInf s ↔ b ∈ lowerBounds s
• csInf_eq_bot_of_bot_mem 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] [OrderBot α] {s : Set α} (hs : ⊥ ∈ s) : sInf s = ⊥
• csInf_le_csSup_of_nonempty_inter 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s t : Set α} (h : (s ∩ t).Nonempty) (hs : BddBelow s := by bddDefault) (ht : BddAbove t := by bddDefault) : sInf s ≤ sSup t
• csInf_le_iff 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h : BddBelow s) (hs : s.Nonempty) : sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a
• Monotone.map_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] {β : Type u_5} [ConditionallyCompleteLattice β] {f : α → β} (hf : Monotone f) (hs : s.Nonempty) : f (sInf s) = sInf (f '' s)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59