target_inter_inv_preimage_preimage

English

Symmetric version: The target intersect with the preimage of the preimage equals target intersect with s.

Русский

Симметрическая версия: целевая часть пересечена с предобразом предобраза равна целевой части пересечения с s.

LaTeX

$$$e.target \\cap (e^{ -1}(e^{ -1}(s))) = e.target \\cap s$$$

Lean4

theorem target_inter_inv_preimage_preimage (s : Set β) : e.target ∩ e.symm ⁻¹' (e ⁻¹' s) = e.target ∩ s :=
  e.symm.source_inter_preimage_inv_preimage _

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