ne_top — Mathlib

English

Let v1 and v2 be AddValuations that are equivalent (v1 IsEquiv v2). Then for every r in R, v1(r) ≠ ⊤ if and only if v2(r) ≠ ⊤.

Русский

Пусть v1 и v2 — AddValuation, которые эквивалентны (v1 IsEquiv v2). Тогда для каждого r в R выполняется v1(r) ≠ ⊤ тогда и только тогда, когда v2(r) ≠ ⊤.

LaTeX

$$$ (v_1 \\text{ IsEquiv } v_2) \\Rightarrow \\forall r:\\, R,\n v_1(r) \\neq \\top \\iff v_2(r) \\neq \\top. $$$

Lean4

theorem ne_top (h : v₁.IsEquiv v₂) {r : R} : v₁ r ≠ (⊤ : Γ₀) ↔ v₂ r ≠ (⊤ : Γ'₀) :=
  Valuation.IsEquiv.ne_zero h

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