Theorems · Theorem · order theory

isGLB_ciInf

∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α},
  BddBelow (Set.range f) → IsGLB (Set.range f) (⨅ i, f i)

Defined in: Mathlib.Order.ConditionallyCompleteLattice.Indexed
Cited by: 3 results in Mathlib
Foundations: Depth 10 from the axioms · uses no axioms
Assumes: ConditionallyCompleteLattice Nonempty

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Set.rangestatement and proof · cited by 4,705
iInfstatement · cited by 1,690
BddBelowstatement and proof · cited by 401
ConditionallyCompleteLatticestatement and proof · cited by 364
IsGLBstatement · cited by 213
Set.range_nonemptyproof · cited by 84
isGLB_csInfproof · cited by 24

Cited by3

Results whose statement or proof uses this declaration.

le_ciInf_iffproof · cited by 5
BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_isClosedEmbeddingproof · cited by 1
Real.isGLB_of_tendsto_antitone_bddBelowproof · cited by 0