biInf_le_eq_of_antitone — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem biInf_le_eq_of_antitone [Preorder β] {f : β → α} (hf : Antitone f) (b : β) : ⨅ (b' ≤ b), f b' = f b :=
  biSup_le_eq_of_monotone (α := αᵒᵈ) hf.dual_right b

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