Almost disjoint families

Definition\(\kappa\)-almost disjoint family of sets#✓fully proved

A family F ⊆ 𝒫(I) is κ-almost disjoint if |A| = κ for every A ∈ F and |A ∩ B| < κ for all distinct A, B ∈ F.

def IsAlmostDisjointFamilyKappa.{u} {I : Type u} (κ : Cardinal) (F : Set (Set I)) : Prop :=
  (∀ A ∈ F, #A = κ) ∧
  (∀ A ∈ F, ∀ B ∈ F, A ≠ B → #((A ∩ B : Set I)) < κ)

DefinitionFunctions almost disjoint modulo the nonstationary ideal#✓fully proved

Functions f, g ∈ ∏_{α<ω₁} A_α are almost disjoint mod the nonstationary ideal if the set { α < ω₁ : f(α) = g(α) } on which they agree is nonstationary in ω₁.

def AlmostDisjointModNS.{u} {A : Set.Iio (aleph 1 : Cardinal.{u}).ord → Type u}
    (f g : (α : Set.Iio (aleph 1 : Cardinal.{u}).ord) → A α) : Prop :=
  ¬ IsStationary {α : Set.Iio (aleph 1 : Cardinal.{u}).ord | f α = g α}

DefinitionAlmost disjoint family of functions on a regular cardinal#✓fully proved

Let κ be a regular cardinal. A family of functions κ → κ is almost disjoint if for all f and g in the family with f≠ g, |{ α ∣ f(α ) = g(α ) }|<κ..

def IsAlmostDisjointFunFamily.{u} {κ : Cardinal.{u}}
    (F : Set (Set.Iio κ.ord → Set.Iio κ.ord)) : Prop :=
  F.Pairwise fun f g => #{α : Set.Iio κ.ord | f α = g α} < Cardinal.lift.{u+1} κ

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.