English
For a maximal ideal I, there exists x with setOfIdeal I = {x}^c, i.e., the ideal is determined by a single point's complement.
Русский
Для максимального идеала I существует x так, что setOfIdeal I = {x}^c; идеал задаётся дополнением к одной точке.
LaTeX
$$$\\exists x: X,\\ setOfIdeal I = \\{x\\}^c$$$
Lean4
/-- The concatenation of two continuous maps defined on adjacent intervals. If the values of the
functions on the common bound do not agree, this is defined as an arbitrarily chosen constant
map. See `concatCM` for the corresponding map on the subtype of compatible function pairs. -/
noncomputable def concat (f : C(Icc a b, E)) (g : C(Icc b c, E)) : C(Icc a c, E) :=
by
by_cases hb : f ⊤ = g ⊥
· let h (t : α) : E := if t ≤ b then IccExtendCM f t else IccExtendCM g t
suffices Continuous h from ⟨fun t => h t, by fun_prop⟩
apply Continuous.if_le (by fun_prop) (by fun_prop) continuous_id continuous_const
rintro x rfl
simpa [IccExtendCM, projIccCM]
·
exact
.const _
(f ⊥) -- junk value
