mk_le_mk_iff — Mathlib

English

For all indices i, and a,b ∈ αi, (⟨i,a⟩ ≤ ⟨i,b⟩) iff a ≤ b, given LE on each αi.

Русский

Для каждого i и a,b∈αi верно: (⟨i,a⟩ ≤ ⟨i,b⟩) эквивалентно a ≤ b, при условии LE на каждом αi.

LaTeX

$$$(\\langle i,a\\rangle \\le \\langle i,b\\rangle) \\iff a \\le b.$$$

Lean4

@[simp]
theorem mk_le_mk_iff [∀ i, LE (α i)] {i : ι} {a b : α i} : (⟨i, a⟩ : Sigma α) ≤ ⟨i, b⟩ ↔ a ≤ b :=
  ⟨fun ⟨_, _, _, h⟩ => h, Sigma.LE.fiber _ _ _⟩

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