mk₂

Mathlib.Data.Set.Constructions

URI: https://scilib.ai/kg/mathlib#FiniteInter.mk₂

← MathLib Explorer

English

Intersections are associative: A ∩ (B ∩ C) = (A ∩ B) ∩ C.

Русский

Пересечения ассоциативны: A ∩ (B ∩ C) = (A ∩ B) ∩ C.

LaTeX

$$$A \cap (B \cap C) = (A \cap B) \cap C$$$

Lean4

theorem mk₂ (h : ∀ ⦃s⦄, s ∈ S → ∀ ⦃t⦄, t ∈ S → s ∩ t ∈ S) : FiniteInter (insert (univ : Set α) S)
    where
  univ_mem := Set.mem_insert Set.univ S
  inter_mem s hs t ht := by aesop

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

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

Разделы

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

Аффилиация

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