disjoint_countablePartition — Mathlib

English

Let α be a type with a countably generated measurable space. For every n and for any s,t ∈ countablePartition α n, if s ≠ t then s and t are disjoint (i.e., s ∩ t = ∅).

Русский

Пусть α — множество с счетно сгенерируемым измеримым пространством. Для любого n и любых s,t ∈ countablePartition α n, если s ≠ t, тогда s и t непересекаются (s ∩ t = ∅).

LaTeX

$$$$ \\forall \\alpha\\, [m:\\\\ MeasurableSpace \\alpha]\\\\, [h:\\\\ CountablyGenerated \\alpha]\\\\, (n:\\\\ Nat)\\\\, \\forall s,t:\\\\ Set \\alpha, \\\\; s \\in countablePartition \\alpha n \\\\; \\land \\\\; t \\in countablePartition \\alpha n \\\\; \\land s \\neq t \\\\Rightarrow \\\\; Disjoint s t. $$$$

Lean4

theorem disjoint_countablePartition {n : ℕ} {s t : Set α} (hs : s ∈ countablePartition α n)
    (ht : t ∈ countablePartition α n) (hst : s ≠ t) : Disjoint s t :=
  disjoint_memPartition _ n hs ht hst

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