HasPropertyB

import Mathlib

/-- A family `(A_i)_{i ∈ I}` of subsets of `α` has **Property B** if there exists
a 2-colouring `f : α → Fin 2` such that no `A_i` is monochromatic. -/
def HasPropertyB {α : Type*} (I : Type*) (A : I → Set α) : Prop :=
  ∃ f : α → Fin 2, ∀ i, ¬IsMonochromatic f (A i)