X_eq_of_equiv — Mathlib

English

If P ≈ Q for Fin 3 → R, then the product relation P_x Q_z^2 = Q_x P_z^2 holds: the X-coordinate relation is preserved under unit scaling along the equivalence.

Русский

Пусть P ≈ Q для функций Fin 3 → R. Тогда выполняется P_x Q_z^2 = Q_x P_z^2: отношение по X сохраняется при ед. масштабировании в эквивалентности.

LaTeX

$$$\forall P,Q: \mathrm{Fin}\,3 \to R,\ (P \approx Q)\Rightarrow P_x \cdot Q_z^{2} = Q_x \cdot P_z^{2}$$$

Lean4

theorem X_eq_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : P x * Q z ^ 2 = Q x * P z ^ 2 :=
  by
  rcases h with ⟨u, rfl⟩
  simp only [Units.smul_def, smul_fin3_ext]
  ring1

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