Theorems · Theorem · general topology

TopologicalSpace.Clopens.mk.congr_simp

∀ {α : Type u_4} [inst : TopologicalSpace α] (carrier carrier_1 : Set α) (e_carrier : carrier = carrier_1)
  (isClopen' : IsClopen carrier),
  { carrier := carrier, isClopen' := isClopen' } = { carrier := carrier_1, isClopen' := ⋯ }

Defined in

Mathlib.Topology.LocallyConstant.Basic

Cited by

2 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

TopologicalSpace