locallyConstant_eq_of_fiber_zero_eq

English

Two locally constant maps f,g: X → Fin(2) are equal if their zero-fiber (preimage of {0}) coincide.

Русский

Два локально константных отображения f,g: X → Fin(2) равны, если совпадает их нулевая фибра.

LaTeX

$$$f,g:\\\\mathrm{LocallyConstant}(X,\\\\mathrm{Fin}(2))\\, (f^{-1}(\\{0\\}) = g^{-1}(\\{0\\}) \\Rightarrow f=g)$$$

Lean4

theorem locallyConstant_eq_of_fiber_zero_eq {X : Type*} [TopologicalSpace X] (f g : LocallyConstant X (Fin 2))
    (h : f ⁻¹' ({0} : Set (Fin 2)) = g ⁻¹' {0}) : f = g :=
  by
  simp only [Set.ext_iff, mem_singleton_iff, mem_preimage] at h
  ext1 x
  exact Fin.fin_two_eq_of_eq_zero_iff (h x)

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