Near-litters

In this file, we define near-litters.

Main declarations

• ConNF.NearLitter: The type of near-litters.
• ConNF.card_nearLitter: There are precisely μ near-litters.
• ConNF.Interference: The interference of two near-litters, which is equal to their symmetric difference if the two near-litters are near, and equal to their intersection if they are not.

structure ConNF.NearLitter [ConNF.Params] : Type u

• litter : ConNF.Litter
• atoms : Set ConNF.Atom
• atoms_near_litter' : self.atoms ~ self.litterᴬ

instance ConNF.instSuperLNearLitterLitter [ConNF.Params] : ConNF.SuperL ConNF.NearLitter ConNF.Litter

Equations

• ConNF.instSuperLNearLitterLitter = { superL := fun (N : ConNF.NearLitter) => N.litter }

instance ConNF.instSuperANearLitterSetAtom [ConNF.Params] : ConNF.SuperA ConNF.NearLitter (Set ConNF.Atom)

Equations

• ConNF.instSuperANearLitterSetAtom = { superA := fun (N : ConNF.NearLitter) => N.atoms }

instance ConNF.instSuperNLitterNearLitter [ConNF.Params] : ConNF.SuperN ConNF.Litter ConNF.NearLitter

Equations

• ConNF.instSuperNLitterNearLitter = { superN := fun (L : ConNF.Litter) => { litter := L, atoms := Lᴬ, atoms_near_litter' := ⋯ } }

@[simp]

theorem ConNF.NearLitter.mk_litter [ConNF.Params] (L : ConNF.Litter) (s : Set ConNF.Atom) (h : s ~ Lᴬ) : { litter := L, atoms := s, atoms_near_litter' := h }ᴸ = L

@[simp]

theorem ConNF.NearLitter.mk_atoms [ConNF.Params] (L : ConNF.Litter) (s : Set ConNF.Atom) (h : s ~ Lᴬ) : { litter := L, atoms := s, atoms_near_litter' := h }ᴬ = s

theorem ConNF.NearLitter.atoms_near_litter [ConNF.Params] (N : ConNF.NearLitter) : Nᴬ ~ Nᴸᴬ

theorem ConNF.NearLitter.symmDiff_small [ConNF.Params] (N : ConNF.NearLitter) : ConNF.Small (symmDiff Nᴬ Nᴸᴬ)

theorem ConNF.NearLitter.diff_small [ConNF.Params] (N : ConNF.NearLitter) : ConNF.Small (Nᴬ \ Nᴸᴬ)

theorem ConNF.NearLitter.diff_small' [ConNF.Params] (N : ConNF.NearLitter) : ConNF.Small (Nᴸᴬ \ Nᴬ)

theorem ConNF.NearLitter.card_atoms [ConNF.Params] (N : ConNF.NearLitter) : Cardinal.mk ↑Nᴬ = Cardinal.mk ConNF.κ

theorem ConNF.NearLitter.atoms_not_small [ConNF.Params] (N : ConNF.NearLitter) : ¬ConNF.Small Nᴬ

theorem ConNF.nearLitter_litter_eq_of_near [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : N₁ᴬ ~ N₂ᴬ) : N₁ᴸ = N₂ᴸ

theorem ConNF.near_of_litter_eq [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : N₁ᴸ = N₂ᴸ) : N₁ᴬ ~ N₂ᴬ

@[simp]

theorem ConNF.nearLitter_near_iff [ConNF.Params] (N₁ N₂ : ConNF.NearLitter) : N₁ᴬ ~ N₂ᴬ ↔ N₁ᴸ = N₂ᴸ

theorem ConNF.NearLitter.ext [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : N₁ᴬ = N₂ᴬ) : N₁ = N₂

theorem ConNF.card_near_litter [ConNF.Params] (L : ConNF.Litter) : Cardinal.mk ↑{s : Set ConNF.Atom | s ~ Lᴬ} = Cardinal.mk ConNF.μ

def ConNF.nearLitterEquiv [ConNF.Params] : ConNF.NearLitter ≃ (L : ConNF.Litter) × ↑{s : Set ConNF.Atom | s ~ Lᴬ}

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConNF.card_nearLitter [ConNF.Params] : Cardinal.mk ConNF.NearLitter = Cardinal.mk ConNF.μ

Interference of near-litters

theorem ConNF.litter_eq_iff_symmDiff_small [ConNF.Params] (N₁ N₂ : ConNF.NearLitter) : N₁ᴸ = N₂ᴸ ↔ ConNF.Small (symmDiff N₁ᴬ N₂ᴬ)

theorem ConNF.litter_ne_of_inter_small [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : ConNF.Small (N₁ᴬ ∩ N₂ᴬ)) : N₁ᴸ ≠ N₂ᴸ

theorem ConNF.inter_small_of_litter_ne [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : N₁ᴸ ≠ N₂ᴸ) : ConNF.Small (N₁ᴬ ∩ N₂ᴬ)

theorem ConNF.litter_ne_iff_inter_small [ConNF.Params] (N₁ N₂ : ConNF.NearLitter) : N₁ᴸ ≠ N₂ᴸ ↔ ConNF.Small (N₁ᴬ ∩ N₂ᴬ)

def ConNF.interference [ConNF.Params] (N₁ N₂ : ConNF.NearLitter) : Set ConNF.Atom

Equations

• ConNF.interference N₁ N₂ = {a : ConNF.Atom | N₁ᴸ = N₂ᴸ ↔ ¬(a ∈ N₁ᴬ ↔ a ∈ N₂ᴬ)} ∩ (N₁ᴬ ∪ N₂ᴬ)

theorem ConNF.interference_eq_of_litter_eq [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : N₁ᴸ = N₂ᴸ) : ConNF.interference N₁ N₂ = symmDiff N₁ᴬ N₂ᴬ

theorem ConNF.interference_eq_of_litter_ne [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : N₁ᴸ ≠ N₂ᴸ) : ConNF.interference N₁ N₂ = N₁ᴬ ∩ N₂ᴬ

theorem ConNF.interference_small [ConNF.Params] (N₁ N₂ : ConNF.NearLitter) : ConNF.Small (ConNF.interference N₁ N₂)