iInf_eq_of_forall_ge_of_forall_gt_exists_lt

English

Let f : ι → α and b ∈ α. If ∀ i, b ≤ f(i) and ∀ w, b < w → ∃ i, f(i) < w, then ⨅ i, f(i) = b.

Русский

Пусть f : ι → α и b ∈ α. Если ∀ i, b ≤ f(i) и ∀ w, b < w → ∃ i, f(i) < w, тогда ⨅ i, f(i) = b.

LaTeX

$$$$\left( \forall i,\; b \le f(i) \right) \rightarrow \left( \forall w,\; b < w \rightarrow \exists i, f(i) < w \right) \rightarrow \bigwedge_{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 `ciInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in conditionally complete
lattices. -/
theorem iInf_eq_of_forall_ge_of_forall_gt_exists_lt : (∀ i, b ≤ f i) → (∀ w, b < w → ∃ i, f i < w) → ⨅ i, f i = b :=
  @iSup_eq_of_forall_le_of_forall_lt_exists_gt αᵒᵈ _ _ _ _

Похожие утверждения