ciSup_Iic — Mathlib

English

For a Preorder β and monotone f: β → α, the supremum over the downward set Iic a is f(a).

Русский

Для предуровня β и монотонной функции f: β → α, верхняя грань по подмножеству Iic a равна f(a).

LaTeX

$$$\sup_{x \in Iic(a)} f(x) = f(a).$$$

Lean4

theorem ciSup_Iic [Preorder β] {f : β → α} (a : β) (hf : Monotone f) : ⨆ x : Iic a, f x = f a :=
  by
  have H : BddAbove (range fun x : Iic a ↦ f x) := ⟨f a, fun _ ↦ by aesop⟩
  apply (le_ciSup H (⟨a, le_refl a⟩ : Iic a)).antisymm'
  rw [ciSup_le_iff H]
  rintro ⟨a, h⟩
  exact hf h

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