shadow_mono

Mathlib.Combinatorics.SetFamily.Shadow

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

English

An alternative monotonicity form: if 𝒜 ⊆ ℬ then ∂𝒜 ⊆ ∂ℬ.

Русский

Альтернативная форма монотонности: если 𝒜 ⊆ ℬ, то ∂𝒜 ⊆ ∂ℬ.

LaTeX

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

Lean4

@[gcongr]
theorem shadow_mono (h𝒜ℬ : 𝒜 ⊆ ℬ) : ∂ 𝒜 ⊆ ∂ ℬ :=
  shadow_monotone h𝒜ℬ

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

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

Разделы

Аффилиация

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