Theorems · Theorem · order theory
iInf_of_isEmpty
∀ {α : Type u_8} {ι : Sort u_9} [inst : InfSet α] [IsEmpty ι] (f : ι → α), iInf f = sInf ∅- Defined in
- Mathlib.Order.CompleteLattice.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- iInfstatement · cited by 1,690
- InfSet.sInfstatement and proof · cited by 935
- IsEmptystatement and proof · cited by 759
- InfSetstatement and proof · cited by 145
- Set.range_eq_emptyproof · cited by 14
Cited by10
Results whose statement or proof uses this declaration.
- iInf_of_emptyproof · cited by 12
- Nat.iInf_of_emptyproof · cited by 3
- NNReal.iInf_emptyproof · cited by 2
- Subspace.dualAnnihilator_iInf_eqproof · cited by 1
- BddBelow.range_iInf_of_iUnion_rangeproof · cited by 1
- Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsToproof · cited by 1
- cbiInf_eq_of_forall_notproof · cited by 1
- Real.iInf_of_isEmptyproof · cited by 1
- ENat.iInf_eq_natCast_iffproof · cited by 1
- Directed.ciInf_monoproof · cited by 0