source_inter_preimage_target_inter

English

The target intersect with the double preimage under e is equal to the target intersect with s.

Русский

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

LaTeX

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

Lean4

theorem source_inter_preimage_target_inter (s : Set β) : e.source ∩ e ⁻¹' (e.target ∩ s) = e.source ∩ e ⁻¹' s :=
  ext fun _ => ⟨fun hx => ⟨hx.1, hx.2.2⟩, fun hx => ⟨hx.1, e.map_source hx.1, hx.2⟩⟩

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