disjoint_sUnion_right

Mathlib.Data.Set.Lattice

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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