English
Let α be a ConditionallyCompleteLattice and b ∈ α. Let f : ι → α be a function indexed by a nonempty ι. If b ≤ f(i) for all i and for every w > b there exists i with f(i) < w, then the infimum of f is b.
Русский
Пусть α — частично упорядоченная условно полная решетка, и задана функция f: ι → α над непустым ι. Если b ≤ f(i) для всех i и для любого w > b существует i с f(i) < w, то инфиму́м f равен b.
LaTeX
$$$\text{If }(\forall i, b \le f(i)) \ \text{and } (\forall w, b < w \rightarrow \exists i, f(i) < w), \text{ then } \inf_{i} f(i) = b.$$$
Lean4
/-- 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. -/
theorem ciInf_eq_of_forall_ge_of_forall_gt_exists_lt [Nonempty ι] {f : ι → α} (h₁ : ∀ i, b ≤ f i)
(h₂ : ∀ w, b < w → ∃ i, f i < w) : ⨅ i : ι, f i = b :=
ciSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ) h₁ h₂
