coe_equiv_apply_eq_preimage — Mathlib

English

The image of a compact set under a homeomorphism can also be expressed as a preimage under the inverse homeomorphism: (Compacts.equiv f K : Set β) = f.symm ⁻¹' (K : Set α).

Русский

Образ компактного множества под гомеоморфизмом можно выразить через предобраз под его обратным гомеоморфизмом: (Compacts.equiv f K : Set β) = f.symm ⁻¹' (K : Set α).

LaTeX

$$$\\forall {f : \\alpha \\equiv_{\\mathrm{t}} \\beta} {K : \\mathrm{Compacts}(\\alpha)},\\\\ (Compacts.equiv f K : \\text{Set }\\beta) = f.symm ^{-1}' (K : \\text{Set }\\alpha)$$$

Lean4

/-- The image of a compact set under a homeomorphism can also be expressed as a preimage. -/
theorem coe_equiv_apply_eq_preimage (f : α ≃ₜ β) (K : Compacts α) :
    (Compacts.equiv f K : Set β) = f.symm ⁻¹' (K : Set α) :=
  f.toEquiv.image_eq_preimage K

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