source_inter_preimage_inv_preimage

English

The set e.source ∩ e^{-1}'(e.target ∩ s) equals e.source ∩ e^{-1}' s.

Русский

Множество e.source ∩ e^{-1}'(e.target ∩ s) равно e.source ∩ e^{-1}' s.

LaTeX

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

Lean4

theorem source_inter_preimage_inv_preimage (s : Set α) : e.source ∩ e ⁻¹' (e.symm ⁻¹' s) = e.source ∩ s :=
  Set.ext fun x => and_congr_right_iff.2 fun hx => by simp only [mem_preimage, e.left_inv hx]

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