mono_left

Mathlib.Combinatorics.SetFamily.Shatter

URI: https://scilib.ai/kg/mathlib#Finset.Shatters.mono_left

English

If 𝒜 ⊆ ℬ and 𝒜.Shatters s, then ℬ.Shatters s.

Русский

Если 𝒜 ⊆ ℬ и 𝒜.Shatters s, тогда ℬ.Shatters s.

LaTeX

$$$ (\mathcal{A} \subseteq \mathcal{B}) \Rightarrow ( \mathcal{A}.Shatters(s) \Rightarrow \mathcal{B}.Shatters(s) ) $$$

Lean4

theorem mono_left (h : 𝒜 ⊆ ℬ) (h𝒜 : 𝒜.Shatters s) : ℬ.Shatters s := fun _t ht ↦
  let ⟨u, hu, hut⟩ := h𝒜 ht;
  ⟨u, h hu, hut⟩

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

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

Разделы

Аффилиация

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