mono_right

Mathlib.Combinatorics.SetFamily.Shatter

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$ t \subseteq s \Rightarrow ( 𝒜.Shatters(s) \Rightarrow 𝒜.Shatters(t) ) $$$

Lean4

theorem mono_right (h : t ⊆ s) (hs : 𝒜.Shatters s) : 𝒜.Shatters t := fun u hu ↦ by
  obtain ⟨v, hv, rfl⟩ := hs (hu.trans h); exact ⟨v, hv, inf_congr_right hu <| inf_le_of_left_le h⟩

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

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

Разделы

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

Аффилиация

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