le_inf' — Mathlib

English

If for all b ∈ s, a ≤ f(b), then a ≤ s.inf' H f; equivalently, a lower-bounds s.inf' f.

Русский

Если для всех b ∈ s выполняется a ≤ f(b), то a ≤ inf' H f; инфимума является наимольшей нижней границей.

LaTeX

$$$\\big( \\forall b \\in s, a \\le f(b) \\big) \\rightarrow a \\le s.inf' H f$$$

Lean4

theorem le_inf' {a : α} (hs : ∀ b ∈ s, a ≤ f b) : a ≤ s.inf' H f :=
  sup'_le (α := αᵒᵈ) H f hs

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