ofIsClopen_fiber_zero — Mathlib

English

If U is clopen, the fiber of the indicator LocallyConstant.ofIsClopen(hU) at 0 is exactly U.

Русский

Если U является как открытым, так и закрытым, то волокно индикатора LocallyConstant.ofIsClopen(hU) при 0 равно U.

LaTeX

$$$\\mathrm{Set.preimage}(\\mathrm{LocallyConstant.instFunLike.coe}(\\mathrm{LocallyConstant.ofIsClopen}~hU), \\{0\\}) = U$$$

Lean4

@[simp]
theorem ofIsClopen_fiber_zero {X : Type*} [TopologicalSpace X] {U : Set X} [∀ x, Decidable (x ∈ U)] (hU : IsClopen U) :
    ofIsClopen hU ⁻¹' ({0} : Set (Fin 2)) = U := by
  ext
  simp only [ofIsClopen, mem_singleton_iff, Fin.one_eq_zero_iff, coe_mk, mem_preimage, ite_eq_left_iff,
    Nat.succ_succ_ne_one]
  tauto

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