mem_upperBounds_image — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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