sup_mul₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso

URI: https://scilib.ai/kg/mathlib#sup_mul₀

← MathLib Explorer

English

Symmetry for right multiplication order isomorphism.

Русский

Симметрия для правого умножения и изоморфизм порядка.

LaTeX

$$OrderIso.mulRight₀_symm( a, ha )$$

Lean4

theorem sup_mul₀ [SemilatticeSup G₀] [MulPosReflectLT G₀] {c : G₀} (hc : 0 ≤ c) (a b : G₀) :
    (a ⊔ b) * c = a * c ⊔ b * c := by
  obtain (rfl | hc) := hc.eq_or_lt
  · simp
  · exact (OrderIso.mulRight₀ c hc).map_sup a b

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

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

Разделы

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

Аффилиация

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