shadow_monotone

Mathlib.Combinatorics.SetFamily.Shadow

URI: https://scilib.ai/kg/mathlib#Finset.shadow_monotone

English

Shadow is monotone: if 𝒜 ⊆ ℬ then ∂𝒜 ⊆ ∂ℬ.

Русский

Тень монотонна: если 𝒜 ⊆ ℬ, то ∂𝒜 ⊆ ∂ℬ.

LaTeX

$$$$ 𝒜 \\subseteq ℬ \\Rightarrow ∂𝒜 \\subseteq ∂ℬ $$$$

Lean4

/-- The shadow is monotone. -/
@[mono]
theorem shadow_monotone : Monotone (shadow : Finset (Finset α) → Finset (Finset α)) := fun _ _ => sup_mono

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

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

Разделы

Аффилиация

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