mem_lowerBounds_image — Mathlib

English

For a strictly antitone f, f a ∈ lowerBounds (f'' s) iff a ∈ upperBounds s.

Русский

Для строго антитонной f: f(a) принадлежит нижним границам образа ⇔ a принадлежит верхним границам s.

LaTeX

$$$ f a \in \mathrm{LB}(f''(s)) \iff a \in \mathrm{UB}(s) $$$

Lean4

theorem mem_lowerBounds_image (hf : StrictAnti f) : f a ∈ lowerBounds (f '' s) ↔ a ∈ upperBounds s := by
  simp [upperBounds, lowerBounds, hf.le_iff_ge]

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