inf_eq_of_min — Mathlib

English

Let α be nonempty and b ∈ range D with hmem: D^{-1}(b) ∈ s and hmin: ∀ a ∈ s, b ≤ D(a). Then s.inf D = b.

Русский

Пусть α непусто и b ∈ range(D) при условии hmem: D^{-1}(b) ∈ s и hmin: ∀ a ∈ s, b ≤ D(a). Тогда s.inf D = b.

LaTeX

$$$b \\in \\mathrm{range}(D) \\land D^{-1}(b) \\in s \\land \\forall a \\in s,\\ b \\le D(a) \\Rightarrow s.inf D = b$$$

Lean4

theorem inf_eq_of_min [Nonempty α] {b : β} (hb : b ∈ Set.range D) (hmem : D.invFun b ∈ s) (hmin : ∀ a ∈ s, b ≤ D a) :
    s.inf D = b :=
  sup_eq_of_max (α := αᵒᵈ) (β := βᵒᵈ) hb hmem hmin

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