disjoint_sUnion_left

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.disjoint_sUnion_left

English

Disjoint (⋃₀ S) t iff ∀ s ∈ S, Disjoint s t.

Русский

Дисjoint ⋃₀ S с t эквивалентно ∀ s ∈ S, Disjoint s t.

LaTeX

$$$$\\mathrm{Disjoint}\\left(\\bigcup_{S\\in S} S, t\\right) \\iff \\forall s \\in S, \\mathrm{Disjoint}(s,t).$$$$

Lean4

@[simp]
theorem disjoint_sUnion_left {S : Set (Set α)} {t : Set α} : Disjoint (⋃₀ S) t ↔ ∀ s ∈ S, Disjoint s t :=
  sSup_disjoint_iff

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

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

Разделы

Аффилиация

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