Theorems · Theorem · order theory

ciInf_eq_of_forall_ge_of_forall_gt_exists_lt

∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {b : α} [Nonempty ι] {f : ι → α},
  (∀ (i : ι), b ≤ f i) → (∀ (w : α), b < w → ∃ i, f i < w) → ⨅ i, f i = b

Introduction rule to prove that b is the infimum of f: it suffices to check that b is smaller than f i for all i, and that this is not the case of any w>b. See iInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in complete lattices.

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Indexed

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ConditionallyCompleteLatticeNonempty