preimage_symm — Mathlib

English

For a ContinuousAffineEquiv f, and any subset s of P₁, the preimage under the inverse equals the image under f of s.

Русский

Для непрерывно аффинного взаимнооднозначного отображения f и любого подмножества s ⊆ P₁ выполняется f.symm ⁻¹' s = f '' s.

LaTeX

$$$\operatorname{Set.preimage}(f^{\mathrm{symm}})(s) = \operatorname{Set.image}(f)(s)$$$

Lean4

@[simp]
theorem preimage_symm (f : P₁ ≃ᴬ[k] P₂) (s : Set P₁) : f.symm ⁻¹' s = f '' s :=
  (f.symm.image_symm _).symm

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