bddAbove_image — Mathlib

English

For a bijection e with order structure, the image of a set under e has the same bounded-above property as the original set: BddAbove(e''s) ↔ BddAbove(s).

Русский

Пусть e — биекция, сохраняющая порядок. Точное множество образа сохраняет верхнюю ограниченность: BddAbove(e''s) ⇔ BddAbove(s).

LaTeX

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

Lean4

@[simp]
theorem bddAbove_image (e : α ≃o β) {s : Set α} : BddAbove (e '' s) ↔ BddAbove s :=
  e.to_galoisConnection.bddAbove_l_image

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