lt_iInf_iff — Mathlib

English

For a ∈ α and f : ι → α, a < iInf f if and only if there exists b with a < b and b ≤ f i for all i.

Русский

Для a ∈ α и f : ι → α верно, что a < iInf f тогда, когда существует b с a < b и b ≤ f(i) для всех i.

LaTeX

$$$\\\\left( a < iInf f \\\\right) \\\\Leftrightarrow \\\\exists b, a < b \\\\wedge \\\\forall i, b \\\\le f i$$$

Lean4

theorem lt_iInf_iff : a < iInf f ↔ ∃ b, a < b ∧ ∀ i, b ≤ f i :=
  ⟨fun h => ⟨iInf f, h, iInf_le f⟩, fun ⟨_, h, hb⟩ => h.trans_le <| le_iInf hb⟩

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