ne_zero — Mathlib

English

If M' is nontrivial, a conformal map f' is not the zero map, i.e., f' ≠ 0.

Русский

Если пространство M' ненулевое, конформное отображение f' не нулевое: f' ≠ 0.

LaTeX

$$$IsConformalMap f'\Rightarrow f' \neq 0$ (assuming $M'$ is nontrivial)$$

Lean4

theorem ne_zero [Nontrivial M'] {f' : M' →L[R] N} (hf' : IsConformalMap f') : f' ≠ 0 :=
  by
  rintro rfl
  rcases exists_ne (0 : M') with ⟨a, ha⟩
  exact ha (hf'.injective rfl)

Похожие утверждения