English
Extensionality lemma: if two ENormedSpaces have equal norm maps, they are equal.
Русский
Лемма экстенсиональности: если два ENormedSpace имеют одинаковые отображения нормы, они равны.
LaTeX
$$⊢ ∀ {e1 e2}, (∀ x, e1 x = e2 x) → e1 = e2$$
Lean4
/-- The `ENormedSpace` sending each non-zero vector to infinity. -/
noncomputable instance : Top (ENormedSpace 𝕜 V) :=
⟨{ toFun := fun x => open scoped Classical in if x = 0 then 0 else ⊤
eq_zero' := fun x => by split_ifs <;> simp [*]
map_add_le' := fun x y => by
split_ifs with hxy hx hy hy hx hy hy <;> try simp [*]
simp [hx, hy] at hxy
map_smul_le' := fun c x =>
by
split_ifs with hcx hx hx <;> simp only [smul_eq_zero, not_or] at hcx
· simp only [mul_zero, le_refl]
· have : c = 0 := by tauto
simp [this]
· tauto
· simpa [mul_top'] using hcx.1 }⟩
