Near-litters

In this file, we define near-litters, which are sets with small symmetric difference to a litter.

Main declarations

• ConNF.IsNearLitter: Proposition stating that a set is near a given litter.
• ConNF.NearLitter: The type of near-litters.
• ConNF.Litter.toNearLitter: Converts a litter to its corresponding near-litter.
• ConNF.NearLitter.IsLitter: Proposition stating that a near-litter comes directly from a litter: it is of the form L.toNearLitter for some litter L.

def ConNF.IsNearLitter [ConNF.Params] (L : ConNF.Litter) (s : Set ConNF.Atom) : Prop

A L-near-litter is a set of small symmetric difference to litter L. In other words, it is near litter L.

Note that here we keep track of which litter a set is near; a set cannot be merely a near-litter, it must be an L-near-litter for some L. A priori, a set could be an L₁-near-litter and also a L₂-near-litter, but this is not the case.

Equations

• ConNF.IsNearLitter L s = ConNF.IsNear (ConNF.litterSet L) s

theorem ConNF.isNearLitter_litterSet [ConNF.Params] (L : ConNF.Litter) : ConNF.IsNearLitter L (ConNF.litterSet L)

The litter set corresponding to L is a near-litter to litter L.

@[simp]

theorem ConNF.isNear_litterSet [ConNF.Params] {L : ConNF.Litter} {s : Set ConNF.Atom} : ConNF.IsNear (ConNF.litterSet L) s ↔ ConNF.IsNearLitter L s

theorem ConNF.IsNearLitter.near [ConNF.Params] {L : ConNF.Litter} {s : Set ConNF.Atom} {t : Set ConNF.Atom} (hs : ConNF.IsNearLitter L s) (ht : ConNF.IsNearLitter L t) : ConNF.IsNear s t

If two sets are L-near-litters, they are near each other. This is because they are both near litter L, and nearness is transitive.

theorem ConNF.IsNearLitter.mk_eq_κ [ConNF.Params] {L : ConNF.Litter} {s : Set ConNF.Atom} (hs : ConNF.IsNearLitter L s) : Cardinal.mk ↑s = Cardinal.mk ConNF.κ

theorem ConNF.IsNearLitter.nonempty [ConNF.Params] {L : ConNF.Litter} {s : Set ConNF.Atom} (hs : ConNF.IsNearLitter L s) : s.Nonempty

@[simp]

theorem ConNF.isNearLitter_litterSet_iff [ConNF.Params] {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} : ConNF.IsNearLitter L₁ (ConNF.litterSet L₂) ↔ L₁ = L₂

A litter set is only a near-litter to itself.

theorem ConNF.IsNearLitter.unique [ConNF.Params] {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} {s : Set ConNF.Atom} (h₁ : ConNF.IsNearLitter L₁ s) (h₂ : ConNF.IsNearLitter L₂ s) : L₁ = L₂

A set is near at most one litter.

@[simp]

theorem ConNF.mk_nearLitter' [ConNF.Params] (L : ConNF.Litter) : Cardinal.mk { s : Set ConNF.Atom // ConNF.IsNearLitter L s } = Cardinal.mk ConNF.μ

There are μ near-litters to litter L.

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

The type of near-litters. A near-litter is a litter together with a set near it.

Equations

• ConNF.NearLitter = ((L : ConNF.Litter) × { s : Set ConNF.Atom // ConNF.IsNearLitter L s })

instance ConNF.NearLitter.instSetLikeAtom [ConNF.Params] : SetLike ConNF.NearLitter ConNF.Atom

Equations

• ConNF.NearLitter.instSetLikeAtom = { coe := fun (N : ConNF.NearLitter) => ↑N.snd, coe_injective' := ⋯ }

@[simp]

theorem ConNF.NearLitter.coe_mk [ConNF.Params] (L : ConNF.Litter) (s : { s : Set ConNF.Atom // ConNF.IsNearLitter L s }) : ↑⟨L, s⟩ = ↑s

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

theorem ConNF.NearLitter.nonempty [ConNF.Params] (N : ConNF.NearLitter) : Nonempty ↥N

@[simp]

theorem ConNF.NearLitter.toProd_fst [ConNF.Params] (N : ConNF.NearLitter) : N.toProd.1 = N.fst

@[simp]

theorem ConNF.NearLitter.toProd_snd [ConNF.Params] (N : ConNF.NearLitter) : N.toProd.2 = ↑N.snd

def ConNF.NearLitter.toProd [ConNF.Params] (N : ConNF.NearLitter) : ConNF.Litter × Set ConNF.Atom

Reinterpret a near-litter as a product of a litter and a set of atoms.

Equations

• N.toProd = (N.fst, ↑N.snd)

theorem ConNF.NearLitter.toProd_injective [ConNF.Params] : Function.Injective ConNF.NearLitter.toProd

@[simp]

theorem ConNF.NearLitter.isNearLitter [ConNF.Params] (N : ConNF.NearLitter) (L : ConNF.Litter) : ConNF.IsNearLitter L ↑N ↔ N.fst = L

A near-litter N is near a given litter L if and only if N has first projection L.

theorem ConNF.NearLitter.isNear_iff_fst_eq_fst [ConNF.Params] (N₁ : ConNF.NearLitter) (N₂ : ConNF.NearLitter) : ConNF.IsNear ↑N₁ ↑N₂ ↔ N₁.fst = N₂.fst

def ConNF.Litter.toNearLitter [ConNF.Params] (L : ConNF.Litter) : ConNF.NearLitter

Convert a litter to its associated near-litter.

Equations

• L.toNearLitter = ⟨L, ⟨ConNF.litterSet L, ⋯⟩⟩

instance ConNF.Litter.instNonemptyNearLitter [ConNF.Params] : Nonempty ConNF.NearLitter

Equations

• ⋯ = ⋯

@[simp]

theorem ConNF.Litter.toNearLitter_fst [ConNF.Params] (L : ConNF.Litter) : L.toNearLitter.fst = L

@[simp]

theorem ConNF.Litter.coe_toNearLitter [ConNF.Params] (L : ConNF.Litter) : ↑L.toNearLitter = ConNF.litterSet L

theorem ConNF.Litter.toNearLitter_injective [ConNF.Params] : Function.Injective ConNF.Litter.toNearLitter

@[simp]

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

There are μ near-litters in total.

@[simp]

theorem ConNF.mk_nearLitter_to [ConNF.Params] (L : ConNF.Litter) : Cardinal.mk ↑{N : ConNF.NearLitter | N.fst = L} = Cardinal.mk ConNF.μ

There aer μ near-litters to a given litter.

inductive ConNF.NearLitter.IsLitter [ConNF.Params] : ConNF.NearLitter → Prop

This near-litter is of the form L.toNearLitter.

• mk: ∀ [inst : ConNF.Params] (L : ConNF.Litter), L.toNearLitter.IsLitter

theorem ConNF.NearLitter.IsLitter.eq_fst_toNearLitter [ConNF.Params] {N : ConNF.NearLitter} (h : N.IsLitter) : N = N.fst.toNearLitter

theorem ConNF.NearLitter.IsLitter.litterSet_eq [ConNF.Params] {N : ConNF.NearLitter} (h : N.IsLitter) : ConNF.litterSet N.fst = ↑N.snd

theorem ConNF.NearLitter.IsLitter.exists_litter_eq [ConNF.Params] {N : ConNF.NearLitter} (h : N.IsLitter) : ∃ (L : ConNF.Litter), N = L.toNearLitter

The main induction rule for near-litters that are litters.

theorem ConNF.NearLitter.not_isLitter [ConNF.Params] {N : ConNF.NearLitter} (h : ¬N.IsLitter) : ConNF.litterSet N.fst ≠ ↑N.snd

theorem ConNF.NearLitter.not_isLitter' [ConNF.Params] {N : ConNF.NearLitter} (h : ¬N.IsLitter) : N.fst.toNearLitter ≠ N

@[simp]

theorem ConNF.mk_nearLitter'' [ConNF.Params] (N : ConNF.NearLitter) : Cardinal.mk ↥N = Cardinal.mk ConNF.κ

The size of each near-litter is κ.

theorem ConNF.symmDiff_union_inter {α : Type u_1} {a : Set α} {b : Set α} : symmDiff a b ∪ a ∩ b = a ∪ b

theorem ConNF.NearLitter.mk_inter_of_fst_eq_fst [ConNF.Params] {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h : N₁.fst = N₂.fst) : Cardinal.mk ↑(↑N₁ ∩ ↑N₂) = Cardinal.mk ConNF.κ

Near-litters to the same litter have κ-sized intersection.

theorem ConNF.NearLitter.inter_nonempty_of_fst_eq_fst [ConNF.Params] {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h : N₁.fst = N₂.fst) : (↑N₁ ∩ ↑N₂).Nonempty

theorem ConNF.NearLitter.inter_small_of_fst_ne_fst [ConNF.Params] {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h : N₁.fst ≠ N₂.fst) : ConNF.Small (↑N₁ ∩ ↑N₂)

Near-litters to different litters have small intersection.