symm — Mathlib

English

If v1 is equivalent to v2, then v2 is equivalent to v1 (symmetry).

Русский

Если v1 эквивалентна v2, то и v2 эквивалентна v1 (симметрия).

LaTeX

$$$ \\forall {R} {\\Gamma_0} {\\Gamma'_0} [\\text{Ring } R] [\\text{LinearOrderedCommMonoidWithZero } \\Gamma_0]\\n {v_1 : Valuation R \\Gamma_0} {v_2 : Valuation R \\Gamma'_0},\\n v_1.IsEquiv v_2 \\to v_2.IsEquiv v_1$$

Lean4

@[symm]
theorem symm (h : v₁.IsEquiv v₂) : v₂.IsEquiv v₁ := fun _ _ => Iff.symm (h _ _)

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