English
For each i, e_i ∈ LocallyConstant(C, ℤ) is defined by e_i(f) = 1 if f(i) = true and 0 otherwise; e_i is locally constant.
Русский
Для каждого i функция e_i: C → ℤ задаётся как e_i(f) = 1, если f(i) = true, и 0 иначе; e_i локально константен.
LaTeX
$$$$ e(i):\\ LocallyConstant\\, C\\, \\mathbb{Z},\\quad e(i)(f)=\\begin{cases}1,& f(i)=1 \\\\ 0,& f(i)=0\\end{cases} $$$$
Lean4
/-- `e C i` is the locally constant map from `C : Set (I → Bool)` to `ℤ` sending `f` to 1 if
`f.val i = true`, and 0 otherwise.
-/
def e (i : I) : LocallyConstant C ℤ
where
toFun := fun f ↦ (if f.val i then 1 else 0)
isLocallyConstant := by
rw [IsLocallyConstant.iff_continuous]
exact
(continuous_of_discreteTopology (f := fun (a : Bool) ↦ (if a then (1 : ℤ) else 0))).comp
((continuous_apply i).comp continuous_subtype_val)
