mulAntidiagonal_mono_right

Mathlib.Data.Set.MulAntidiagonal

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

← MathLib Explorer

English

If t1 is contained in t2, then mulAntidiagonal s t1 a ⊆ mulAntidiagonal s t2 a.

Русский

Если t1 ⊆ t2, то mulAntidiagonal(s, t1, a) ⊆ mulAntidiagonal(s, t2, a).

LaTeX

$$$t_1 \subseteq t_2 \implies mulAntidiagonal\,(s,t_1,a) \subseteq mulAntidiagonal\,(s,t_2,a).$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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