sSupIndep_pair — Mathlib

English

Two-element case with pairwise disjoint criterion is equivalent to the two-element disjointness for any single pair.

Русский

Два элемента — аналогично парам: независимость {a,b} эквивалентна Disjoint a b, и т.д.

LaTeX

$$sSupIndep {a,b} ↔ Disjoint a b$$

Lean4

theorem sSupIndep_pair {a b : α} (hab : a ≠ b) : sSupIndep ({ a, b } : Set α) ↔ Disjoint a b :=
  by
  constructor
  · intro h
    exact h.pairwiseDisjoint (mem_insert _ _) (mem_insert_of_mem _ (mem_singleton _)) hab
  · rintro h c ((rfl : c = a) | (rfl : c = b))
    · convert h using 1
      simp [hab, sSup_singleton]
    · convert h.symm using 1
      simp [hab, sSup_singleton]

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