insert_mem_upShadow

Mathlib.Combinatorics.SetFamily.Shadow

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

English

If s ∈ 𝒜 and a ∉ s, then insert a s ∈ ∂⁺ 𝒜.

Русский

Если s ∈ 𝒜 и a ∉ s, то insert a s ∈ ∂⁺ 𝒜.

LaTeX

$$$ s ∈ 𝒜 \land a \notin s \Rightarrow insert a s ∈ ∂⁺ 𝒜 $$$

Lean4

theorem insert_mem_upShadow (hs : s ∈ 𝒜) (ha : a ∉ s) : insert a s ∈ ∂⁺ 𝒜 :=
  mem_upShadow_iff.2 ⟨s, hs, a, ha, rfl⟩

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

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

Разделы

Аффилиация

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