smulAntidiagonal_mono_left

Mathlib.Data.Set.SMulAntidiagonal

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

← MathLib Explorer

English

If s1 ⊆ s2, then smulAntidiagonal s1 t a ⊆ smulAntidiagonal s2 t a.

Русский

Если s1 ⊆ s2, то smulAntidiagonal s1 t a ⊆ smulAntidiagonal s2 t a.

LaTeX

$$s1 ⊆ s2 → s.smulAntidiagonal t a ⊆ s2.smulAntidiagonal t a$$

Lean4

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

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

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

Разделы

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

Аффилиация

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