English
The product of two normed spaces is a normed space with the sup norm; namely, ‖(x,y)‖ = max{‖x‖, ‖y‖}.
Русский
Произведение двух нормированных пространств является нормированным пространством с верхней нормой: ‖(x,y)‖ = max{‖x‖,‖y‖}.
LaTeX
$$$\\|(x,y)\\| = \\max\\{ \\|x\\|, \\|y\\| \\}$$$
Lean4
instance discreteTopology_zmultiples {E : Type*} [NormedAddCommGroup E] [NormedSpace ℚ E] (e : E) :
DiscreteTopology <| AddSubgroup.zmultiples e :=
by
rcases eq_or_ne e 0 with (rfl | he)
· rw [AddSubgroup.zmultiples_zero_eq_bot]
exact Subsingleton.discreteTopology (α := ↑(⊥ : Subspace ℚ E))
· rw [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]
refine ⟨Metric.ball 0 ‖e‖, Metric.isOpen_ball, ?_⟩
ext ⟨x, hx⟩
obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx
rw [mem_preimage, mem_ball_zero_iff, AddSubgroup.coe_mk, mem_singleton_iff, Subtype.ext_iff, AddSubgroup.coe_mk,
AddSubgroup.coe_zero, norm_zsmul ℚ k e, Int.norm_cast_rat, Int.norm_eq_abs,
mul_lt_iff_lt_one_left (norm_pos_iff.mpr he), ← @Int.cast_one ℝ _, ← Int.cast_abs, Int.cast_lt,
Int.abs_lt_one_iff, smul_eq_zero, or_iff_left he]
