biSup_le_eq_of_monotone — Mathlib

English

Let β be a preorder and f: β → α be monotone. For any b ∈ β, the supremum over all b' ≤ b of f(b') equals f(b).

Русский

Пусть β — предпорядок и f: β → α монотонна. Тогда для любого b верно, что sup_{b' ≤ b} f(b') = f(b).

LaTeX

$$$\\\\bigvee_{b' \\\\le b} f(b') = f(b)$$$

Lean4

theorem biSup_le_eq_of_monotone [Preorder β] {f : β → α} (hf : Monotone f) (b : β) : ⨆ (b' ≤ b), f b' = f b :=
  le_antisymm (iSup₂_le_iff.2 (fun _ hji ↦ hf hji)) (le_iSup_of_le b (ge_of_eq (iSup_pos le_rfl)))

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