smulAntidiagonal_mono_right

Mathlib.Data.Set.SMulAntidiagonal

URI: https://scilib.ai/kg/mathlib#Set.smulAntidiagonal_mono_right

← MathLib Explorer

English

If t1 ⊆ t2, then smulAntidiagonal s t1 a ⊆ smulAntidiagonal s t2 a.

Русский

Если t1 ⊆ t2, то smulAntidiagonal s t1 a ⊆ smulAntidiagonal s t2 a.

LaTeX

$$t1 ⊆ t2 → s.smulAntidiagonal t1 a ⊆ s.smulAntidiagonal t2 a$$

Lean4

@[to_additive]
theorem smulAntidiagonal_mono_right (h : t₁ ⊆ t₂) : smulAntidiagonal s t₁ a ⊆ smulAntidiagonal s t₂ a := fun _ hx =>
  ⟨hx.1, h hx.2.1, hx.2.2⟩

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

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

Разделы

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

Аффилиация

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