bddAbove_preimage — Mathlib

English

For an order isomorphism e, the preimage of a set preserves bounded-above: BddAbove(e^{-1}'s s) ⇔ BddAbove(s).

Русский

Для изоморфизма e предобраз множества сохраняет верхнюю ограниченность: BddAbove(e^{-1}'s s) ⇔ BddAbove(s).

LaTeX

$$$$ BddAbove( e^{-1}' s ) \\;\\Longleftrightarrow\\; BddAbove(s). $$$$

Lean4

@[simp]
theorem bddAbove_preimage (e : α ≃o β) {s : Set β} : BddAbove (e ⁻¹' s) ↔ BddAbove s := by
  rw [← e.bddAbove_image, e.image_preimage]

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