ciInf_Ici — Mathlib

English

For a Preorder β and monotone f: β → α, the infimum over the upper set Ici a is f(a).

Русский

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

LaTeX

$$$\inf_{x \in Ici(a)} f(x) = f(a).$$$

Lean4

theorem ciInf_Ici [Preorder β] {f : β → α} (a : β) (hf : Monotone f) : ⨅ x : Ici a, f x = f a :=
  by
  have H : BddBelow (range fun x : Ici a ↦ f x) := ⟨f a, fun _ ↦ by aesop⟩
  apply (ciInf_le H (⟨a, le_refl a⟩ : Ici a)).antisymm
  rw [le_ciInf_iff H]
  rintro ⟨a, h⟩
  exact hf h

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