sigma_eq_empty

Mathlib.Data.Finset.Sigma

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

← MathLib Explorer

English

If s1 ⊆ s2 and ti ⊆ t2i for all i, then s1.sigma t1 ⊆ s2.sigma t2.

Русский

Если s1 ⊆ s2 и t1 i ⊆ t2 i для всех i, тогда s1.sigma t1 ⊆ s2.sigma t2.

LaTeX

$$s1 ⊆ s2 → (∀ i, t1 i ⊆ t2 i) → s1.sigma t1 ⊆ s2.sigma t2$$

Lean4

@[simp]
theorem sigma_eq_empty : s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅ := by
  simp only [← not_nonempty_iff_eq_empty, sigma_nonempty, not_exists, not_and]

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

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

Разделы

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

Аффилиация

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