upShadow_monotone

Mathlib.Combinatorics.SetFamily.Shadow

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

← MathLib Explorer

English

The upper shadow is monotone: if 𝒜 ⊆ ℬ, then ∂⁺ 𝒜 ⊆ ∂⁺ ℬ.

Русский

Верхняя тень монотонна: если 𝒜 ⊆ ℬ, то ∂⁺ 𝒜 ⊆ ∂⁺ ℬ.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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