symm_preimage_preimage — Mathlib

English

If e is an order isomorphism, then e.symm ⁻¹' (e ⁻¹' s) = s; the preimage under the inverse of the image under e recovers the original set.

Русский

Если e — изоморфизм порядка, то e.symm ⁻¹' (e ⁻¹' s) = s; предобраз под обратным отображением восстанавливает исходное множество.

LaTeX

$$$e.symm^{-1}' (e^{-1}' s) = s$$$

Lean4

@[simp]
theorem symm_preimage_preimage (e : α ≃o β) (s : Set β) : e.symm ⁻¹' (e ⁻¹' s) = s :=
  e.toEquiv.symm_preimage_preimage s

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