English
For any subset s of the base, the preimage under symmetry intersected with the base set corresponds to the product set (s ∩ baseSet) × univ.
Русский
Для любой подмножества s базиса его предобраз под симметрией, пересечённый с базовым множеством, эквивалентен произведению (s ∩ базовое) × универсума.
LaTeX
$$$e.toPartialEquiv.symm^{-1}(proj^{-1}(s))\cap (e.baseSet\times\mathop{univ})=(s\cap e.baseSet)\times\mathop{univ},\quad \forall s\subset B$$$
Lean4
@[simp, mfld_simps]
theorem preimage_symm_proj_inter (s : Set B) :
e.toPartialEquiv.symm ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ = (s ∩ e.baseSet) ×ˢ univ :=
by
ext ⟨x, y⟩
suffices x ∈ e.baseSet → (proj (e.toPartialEquiv.symm (x, y)) ∈ s ↔ x ∈ s) by
simpa only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ, and_congr_left_iff]
intro h
rw [e.proj_symm_apply' h]
