sSupIndep_iff_pairwiseDisjoint — Mathlib

English

In an ordered frame, sSupIndep s is equivalent to s being pairwise disjoint under id.

Русский

В пространстве с упорядочением sSupIndep s эквивалентно тому, что элементы множества s попарно непересекаются под действием идентичности.

LaTeX

$$$\\\\forall α [Order.Frame α],\\\\ sSupIndep s \\\\iff s.PairwiseDisjoint id$$$

Lean4

theorem sSupIndep_iff_pairwiseDisjoint {s : Set α} : sSupIndep s ↔ s.PairwiseDisjoint id :=
  ⟨sSupIndep.pairwiseDisjoint, fun hs _ hi => disjoint_sSup_iff.2 fun _ hj => hs hi hj.1 <| Ne.symm hj.2⟩

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