supIndep_univ_bool — Mathlib

English

On the two-element boolean index set, the SupIndep condition for a function f: Bool → α is equivalent to disjointness of its values at false and true.

Русский

Для двоичного индекса: SupIndep для f: Bool → α эквивалентно тому, что значения f(false) и f(true) несвязаны (Disjoint).

LaTeX

$$$(Finset.univ : Finset Bool).SupIndep f \\iff Disjoint (f False) (f True)$$$

Lean4

theorem supIndep_univ_bool (f : Bool → α) : (Finset.univ : Finset Bool).SupIndep f ↔ Disjoint (f false) (f true) :=
  haveI : true ≠ false := by simp only [Ne, not_false_iff, reduceCtorEq]
  (supIndep_pair this).trans disjoint_comm

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