mono

Mathlib.Combinatorics.Additive.Corner.Defs

URI: https://scilib.ai/kg/mathlib#IsCornerFree.mono

English

If A ⊆ B and IsCornerFree B holds, then IsCornerFree A holds.

Русский

Если A ⊆ B и IsCornerFree B, тогда IsCornerFree A.

LaTeX

$$A ⊆ B ∧ IsCornerFree B ⇒ IsCornerFree A$$

Lean4

theorem mono (hAB : A ⊆ B) (hB : IsCornerFree B) : IsCornerFree A := fun _x₁ _y₁ _x₂ _y₂ hxyd ↦ hB <| hxyd.mono hAB

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

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

Разделы

Аффилиация

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