Fibers of a locally constant function as clopen sets

The fibers f⁻¹{a} of a locally constant function f : X → α are clopen (IsLocallyConstant.isClopen_fiber). This file packages them as elements of Clopens X (LocallyConstant.fiberClopens). Their underlying open sets (f.fiberClopens a).toOpens can index restrictions of sheaves, and they cover X. Their preimages under a continuous map g are the fibers of f ∘ g (LocallyConstant.comap_toOpens_fiberClopens).

def LocallyConstant.fiberClopens {X : Type u_1} {α : Type u_2} [TopologicalSpace X] (f : LocallyConstant X α) (a : α) : TopologicalSpace.Clopens X

The fiber f⁻¹{a} of a locally constant function f, as a clopen subset of X.

@[simp]

theorem LocallyConstant.mem_fiberClopens {X : Type u_1} {α : Type u_2} [TopologicalSpace X] {f : LocallyConstant X α} {a : α} {x : X} : x ∈ f.fiberClopens a ↔ f x = a

@[simp]

theorem LocallyConstant.coe_fiberClopens {X : Type u_1} {α : Type u_2} [TopologicalSpace X] (f : LocallyConstant X α) (a : α) : ↑(f.fiberClopens a) = ⇑f ⁻¹' {a}

theorem LocallyConstant.iSup_toOpens_fiberClopens {X : Type u_1} {α : Type u_2} [TopologicalSpace X] (f : LocallyConstant X α) : ⨆ (a : α), (f.fiberClopens a).toOpens = ⊤

The fibers of a locally constant function, as open sets, cover its domain.

theorem LocallyConstant.comap_toOpens_fiberClopens {X : Type u_1} {α : Type u_2} [TopologicalSpace X] {Y : Type u_3} [TopologicalSpace Y] (g : C(Y, X)) (f : LocallyConstant X α) (a : α) : (TopologicalSpace.Opens.comap g) (f.fiberClopens a).toOpens = ((comap g f).fiberClopens a).toOpens

The preimage under a continuous map g of the fiber of f over a is the fiber of f ∘ g over a.