English
Let ι be an index set and for every i an ordered type π(i) with a preorder. For any x,y ∈ ∀ i, π(i), we have x < y if and only if x ≤ y and there exists i with x(i) < y(i).
Русский
Пусть ι — множество индексов и для каждого i задан предзаказ на π(i). Для X и Y, функции из ι в соответствующие π(i), выполняется X < Y тогда и только тогда, когда X ≤ Y и существует индекс i, такой что X(i) < Y(i).
LaTeX
$$$x < y \leftrightarrow x \le y \land \exists i\; x_i < y_i$$$
Lean4
theorem lt_def [∀ i, Preorder (π i)] {x y : ∀ i, π i} : x < y ↔ x ≤ y ∧ ∃ i, x i < y i := by
simp +contextual [lt_iff_le_not_ge, Pi.le_def]
