English
If for every c in the codomain γ there is an equivalence between the fibers f^{-1}({c}) and g^{-1}({c}), then there exists an equivalence α ≃ β between the domains.
Русский
Если для каждого c в кодомане γ существуют эквивалентности между волокнами f^{-1}({c}) и g^{-1}({c}), то существует эквивалентность между доменами α и β.
LaTeX
$$(∀ c, f^{-1}({c}) ≃ g^{-1}({c})) ⇒ α ≃ β$$
Lean4
theorem preimage_piEquivPiSubtypeProd_symm_pi {α : Type*} {β : α → Type*} (p : α → Prop) [DecidablePred p]
(s : ∀ i, Set (β i)) :
(piEquivPiSubtypeProd p β).symm ⁻¹' pi univ s =
(pi univ fun i : { i // p i } => s i) ×ˢ pi univ fun i : { i // ¬p i } => s i :=
by
ext ⟨f, g⟩
simp only [mem_preimage, mem_univ_pi, prodMk_mem_set_prod_eq, Subtype.forall, ← forall_and]
refine forall_congr' fun i => ?_
dsimp only [Subtype.coe_mk]
by_cases hi : p i <;>
simp [hi]
-- See also `Equiv.sigmaFiberEquiv`.
