mem_finPairsLT — Mathlib

English

Characterization of membership in the finite pair set: an element a is in finPairsLT n iff its second coordinate is less than its first.

Русский

Характеристика принадлежности к множеству пар: a ∈ finPairsLT n тогда и только тогда, когда вторая компонента меньше первой.

LaTeX

$$$ a \\in finPairsLT\\, n \\iff a.2 < a.1 $$$

Lean4

theorem mem_finPairsLT {n : ℕ} {a : Σ _ : Fin n, Fin n} : a ∈ finPairsLT n ↔ a.2 < a.1 := by
  simp only [finPairsLT, Fin.lt_iff_val_lt_val, true_and, mem_attachFin, mem_range, mem_univ, mem_sigma]

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