srel_iff_srel — Mathlib

English

For any a,b ∈ A, algebra_map extension preserves the valuative relation: algebraMap a <ᵥ algebraMap b iff a <ᵥ b.

Русский

Для любых a,b ∈ A отображение по расширению сохраняет валюативное отношение: algebraMap a <ᵥ algebraMap b эквивалентно a <ᵥ b.

LaTeX

$$$\\mathrm{algebraMap}_{A,B}(a) <_{\\mathrm{v}} \\mathrm{algebraMap}_{A,B}(b) \\iff a <_{\\mathrm{v}} b$$$

Lean4

theorem srel_iff_srel (a b : A) : algebraMap A B a <ᵥ algebraMap A B b ↔ a <ᵥ b := by
  rw [srel_iff, rel_iff_rel, srel_iff]

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