bddBelow_image — Mathlib

English

Dual statement to the previous: the image under an order isomorphism preserves bounded-below: BddBelow(e''s) ↔ BddBelow(s).

Русский

Двойственное утверждение к предыдущему: образ сохраняет нижнюю ограниченность: BddBelow(e''s) ⇔ BddBelow(s).

LaTeX

$$$$ BddBelow(e''s) \\;\\Longleftrightarrow\\; BddBelow(s). $$$$

Lean4

@[simp]
theorem bddBelow_image (e : α ≃o β) {s : Set α} : BddBelow (e '' s) ↔ BddBelow s :=
  e.dual.bddAbove_image

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