English
If β is a lattice and a topological lattice, then C_c(α, β) carries a natural lattice structure given pointwise by f ∨ g and f ∧ g, with (f ∨ g)(x) = f(x) ∨ g(x) and (f ∧ g)(x) = f(x) ∧ g(x).
Русский
Если β — решётка и топологическая решётка, то C_c(α, β) естественно наделяется структурой решётки, где (f ∨ g)(x) = f(x) ∨ g(x) и (f ∧ g)(x) = f(x) ∧ g(x).
LaTeX
$$$$ \forall f,g \in C_c(\alpha, β),\ (f \vee g)(x) = f(x) \vee g(x),\ (f \wedge g)(x) = f(x) \wedge g(x) \quad (\text{for all } x). $$$$
Lean4
/-- Composition of a continuous function with compact support with a cocompact map
yields another continuous function with compact support. -/
def comp (f : C_c(γ, δ)) (g : β →co γ) : C_c(β, δ)
where
toContinuousMap := (f : C(γ, δ)).comp g
hasCompactSupport' :=
by
apply
IsCompact.of_isClosed_subset (g.isCompact_preimage_of_isClosed f.2 (isClosed_tsupport _))
(isClosed_tsupport (f ∘ g))
intro x hx
rw [tsupport, Set.mem_preimage, _root_.mem_closure_iff]
intro o ho hgxo
rw [tsupport, _root_.mem_closure_iff] at hx
obtain ⟨y, hy⟩ := hx (g ⁻¹' o) (IsOpen.preimage g.1.2 ho) hgxo
exact ⟨g y, hy⟩
