snd_mono — Mathlib

English

Let α and β be monoids with a preorder. The second-coordinate projection g: α × β → β is monotone; if (a,b) ≤ (a',b'), then b ≤ b'.

Русский

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

LaTeX

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

Lean4

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

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