innerContent_comap — Mathlib

English

For a given homeomorphism f, innerContent respects the comap, μ.innerContent(Opens.comap f U) = μ.innerContent U.

Русский

При гомеоморфизме f внутреннее содержимое сохраняется под обратным образом: μ.innerContent(Opens.comap f U) = μ.innerContent U.

LaTeX

$$$μ.innerContent(Opens.comap f U) = μ.innerContent U$$$

Lean4

theorem innerContent_comap (f : G ≃ₜ G) (h : ∀ ⦃K : Compacts G⦄, μ (K.map f f.continuous) = μ K) (U : Opens G) :
    μ.innerContent (Opens.comap f U) = μ.innerContent U :=
  by
  refine (Compacts.equiv f).surjective.iSup_congr _ fun K => iSup_congr_Prop image_subset_iff ?_
  intro hK
  simp only [Equiv.coe_fn_mk, Compacts.equiv]
  apply h

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