lt_of_strongLT — Mathlib

English

If there exists at least one index i with a_i < b_i and a ≺ b, then a < b in the product preorder when the index set is nonempty.

Русский

Существование индекса с a_i < b_i и слабое отношение между a и b дает a < b в произведении, если множество индексов ненулевое.

LaTeX

$$$\text{StrongLT } a b \Rightarrow a < b$$$

Lean4

theorem lt_of_strongLT [Nonempty ι] (h : a ≺ b) : a < b :=
  by
  inhabit ι
  exact Pi.lt_def.2 ⟨le_of_strongLT h, default, h _⟩

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