fst_mono — Mathlib

English

Let α and β be monoids with a preorder. The first-coordinate projection f: α × β → α is monotone; that is, whenever (a,b) ≤ (a',b'), we have a ≤ a'.

Русский

Пусть α и β — моноиды с частичным порядком. Первая координатная проекция f: α×β → α монотонна: если (a,b) ≤ (a',b'), то a ≤ a'.

LaTeX

$$$$ \forall (a,b),(a',b') \in \alpha \times \beta,\ (a,b) \le (a',b') \Rightarrow a \le a'. $$$$

Lean4

@[to_additive]
theorem fst_mono : Monotone (MonoidHom.fst α β) := fun _ _ ↦ by simp +contextual [Prod.le_def]

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