cast_lt — Mathlib

English

Let p, q be elements of ℚ≥0. Their images under the canonical embedding into K preserve the strict order: (p : K) < q if and only if p < q.

Русский

Пусть p, q ∈ ℚ≥0. Их образы в K через каноническое отображение сохраняют строгое неравенство: (p : K) < q ⇔ p < q.

LaTeX

$$$\forall p,q \in \mathbb{Q}_{\ge 0},\ (p:K) < q \iff p < q$$$

Lean4

@[simp, norm_cast]
theorem cast_lt : (p : K) < q ↔ p < q :=
  cast_strictMono.lt_iff_lt

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