preimage_symm_proj_baseSet — Mathlib

English

The inverse image of the base set under the projection, intersected with the target, equals the target set itself.

Русский

Обратное изображение базового множества через проекцию, пересеченное с областью действия, совпадает с самой областью действия.

LaTeX

$$$e.toPartialEquiv.symm^{-1}(proj^{-1}(e.baseSet))\cap e.target = e.target$$$

Lean4

@[simp, mfld_simps]
theorem preimage_symm_proj_baseSet : e.toPartialEquiv.symm ⁻¹' (proj ⁻¹' e.baseSet) ∩ e.target = e.target :=
  by
  refine inter_eq_right.mpr fun x hx => ?_
  simp only [mem_preimage, e.proj_symm_apply hx]
  exact e.mem_target.mp hx

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