bddBelow_preimage — Mathlib

English

Dual statement: Preimage under an order isomorphism preserves bounded-below: BddBelow(e^{-1}'s s) ⇔ BddBelow(s).

Русский

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

LaTeX

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

Lean4

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

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