Theorems · Theorem · order theory
Directed.ciInf_le_of_le
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] {a : α} {f : ι → α},
Directed (fun x1 x2 => x2 ≤ x1) f → BddBelow (Set.range f) → ∀ (c : ι), f c ≤ a → iInf f ≤ a- Cited by
- 1 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
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
- Directedstatement and proof · cited by 213
- ConditionallyCompletePartialOrderInfstatement and proof · cited by 51
- ge_transproof · cited by 34
- Directed.ciInf_leproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- Directed.ciInf_monoproof · cited by 0