map — Mathlib

English

An induction principle for rays: every ray is generated by some nonzero vector via rayOfNeZero.

Русский

Принцип индукции по лучам: каждый луч порождается ненулевым вектором через rayOfNeZero.

LaTeX

$$$ \forall C:Module.Ray(R,M)\to Prop, (\forall v\, (hv:\, v\neq 0), C(\text{rayOfNeZero}(R,v,hv)))\Rightarrow \forall x, C(x). $$$

Lean4

/-- An equivalence between modules implies an equivalence between rays. -/
def map (e : M ≃ₗ[R] N) : Module.Ray R M ≃ Module.Ray R N :=
  Quotient.congr (RayVector.mapLinearEquiv e) fun _ _ => (SameRay.sameRay_map_iff _).symm

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