fst_mono

Mathlib.Algebra.Order.GroupWithZero.Lex

URI: https://scilib.ai/kg/mathlib#MonoidWithZeroHom.fst_mono

← MathLib Explorer

English

The inr embedding is strictly monotone under injectivity conditions.

Русский

Встраивание inr строго монотонно при условии инъективности.

LaTeX

$$$\text{inr}$ строго монотонно.$$

Lean4

theorem fst_mono [LinearOrderedCommGroupWithZero M₀] [GroupWithZero N₀] [Preorder N₀] : Monotone (fst M₀ N₀) :=
  by
  refine WithZero.forall.mpr ?_
  simp +contextual [WithZero.forall, Prod.le_def]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru