supIndep_univ_fin_two — Mathlib

English

For a function f: Fin 2 → α, the universal Finset of 2 elements is SupIndep iff its two values are disjoint.

Русский

Для f: Fin 2 → α, ∀, множество Fin 2 SupIndep ⇔ Disjoint (f 0) (f 1).

LaTeX

$$$(Finset.univ : Finset (Fin 2)).SupIndep f \\iff Disjoint (f 0) (f 1)$$$

Lean4

@[simp]
theorem supIndep_univ_fin_two (f : Fin 2 → α) : (Finset.univ : Finset (Fin 2)).SupIndep f ↔ Disjoint (f 0) (f 1) :=
  have : (0 : Fin 2) ≠ 1 := by simp
  supIndep_pair this

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