English
There exists a bump covering consisting of a single bump function uniformly equal to one, used as an example for creating an inhabited instance.
Русский
Существует покрытие-бамп, состоящее из единственной функции-бампа, равной единице повсюду, служащего примером для инстанции, удовлетворяющей условиям непрерывности и локальной конечности.
LaTeX
$$$\exists i : \iota,\; \text{BumpCovering.single}(i, s)\text{ has toFun equal to } 1 \text{ and satisfies the local finiteness conditions.}$$$
Lean4
/-- A `BumpCovering` that consists of a single function, uniformly equal to one, defined as an
example for `Inhabited` instance. -/
protected def single (i : ι) (s : Set X) : BumpCovering ι X s
where
toFun := Pi.single i 1
locallyFinite'
x := by
refine ⟨univ, univ_mem, (finite_singleton i).subset ?_⟩
rintro j ⟨x, hx, -⟩
contrapose! hx
rw [mem_singleton_iff] at hx
simp [hx]
nonneg' := le_update_iff.2 ⟨fun _ => zero_le_one, fun _ _ => le_rfl⟩
le_one' := update_le_iff.2 ⟨le_rfl, fun _ _ _ => zero_le_one⟩
eventuallyEq_one' x _ := ⟨i, by rw [Pi.single_eq_same, ContinuousMap.coe_one]⟩
