preimage_closure — Mathlib

English

The preimage of a closure under a continuous linear equivalence equals the closure of the preimage.

Русский

Обратное образ замыкания по непрерывной линейной эквивалентности равно замыканию обратного образа.

LaTeX

$$$ e^{-1}'(\overline{S}) = \overline{e^{-1}'(S)} $$$

Lean4

theorem preimage_closure (e : M₁ ≃SL[σ₁₂] M₂) (s : Set M₂) : e ⁻¹' closure s = closure (e ⁻¹' s) :=
  e.toHomeomorph.preimage_closure s

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