has_union — Mathlib

English

If s1 and s2 are in a Dynkin system and they are disjoint, then their union is also in the Dynkin system.

Русский

Если множества s1 и s2 принадлежат Dynkin-системе и они дизъюнктны, то их объединение также принадлежит системе.

LaTeX

$$$\forall s_1,s_2,\ d.Has(s_1) \land d.Has(s_2) \land Disjoint(s_1,s_2) \Rightarrow d.Has(s_1 \cup s_2)$$$

Lean4

theorem has_union {s₁ s₂ : Set α} (h₁ : d.Has s₁) (h₂ : d.Has s₂) (h : Disjoint s₁ s₂) : d.Has (s₁ ∪ s₂) :=
  by
  rw [union_eq_iUnion]
  exact d.has_iUnion (pairwise_disjoint_on_bool.2 h) (Bool.forall_bool.2 ⟨h₂, h₁⟩)

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