Documentation

ConNF.FOA.Basic.Sublitter

Sublitters #

In this file, we define sublitters.

Main declarations #

source
structure ConNF.Sublitter [ConNF.Params] :
Type u

A sublitter is a co-small subset of a litter set.

Instances For
    source
    theorem ConNF.Sublitter.subset [ConNF.Params] (self : ConNF.Sublitter) :
    self.carrier ⊆ ConNF.litterSet self.litter
    source
    theorem ConNF.Sublitter.diff_small [ConNF.Params] (self : ConNF.Sublitter) :
    ConNF.Small (ConNF.litterSet self.litter \ self.carrier)
    source
    theorem ConNF.Sublitter.mk_S_eq_κ [ConNF.Params] (S : ConNF.Sublitter) :
    Cardinal.mk ↑S.carrier = Cardinal.mk ConNF.κ

    Use sublitter.mk_eq_κ instead if possible.

    source
    instance ConNF.Sublitter.instSetLikeAtom [ConNF.Params] :
    SetLike ConNF.Sublitter ConNF.Atom
    Equations
    • ConNF.Sublitter.instSetLikeAtom = { coe := fun (S : ConNF.Sublitter) => S.carrier, coe_injective' := ⋯ }
    source
    @[simp]
    theorem ConNF.Sublitter.mk_eq_κ [ConNF.Params] (S : ConNF.Sublitter) :
    Cardinal.mk ↥S = Cardinal.mk ConNF.κ
    source
    @[simp]
    theorem ConNF.Sublitter.mk_eq_κ' [ConNF.Params] (S : ConNF.Sublitter) :
    Cardinal.mk ↑↑S = Cardinal.mk ConNF.κ
    source
    @[simp]
    theorem ConNF.Sublitter.carrier_eq_coe [ConNF.Params] {S : ConNF.Sublitter} :
    S.carrier = ↑S
    source
    @[simp]
    theorem ConNF.Sublitter.coe_mk [ConNF.Params] (L : ConNF.Litter) (S : Set ConNF.Atom) (subset : S ⊆ ConNF.litterSet L) (diff_small : ConNF.Small (ConNF.litterSet L \ S)) :
    ↑{ litter := L, carrier := S, subset := subset, diff_small := diff_small } = S
    source
    theorem ConNF.Sublitter.ext [ConNF.Params] {S₁ : ConNF.Sublitter} {S₂ : ConNF.Sublitter} (h : ↑S₁ = ↑S₂) :
    S₁ = S₂
    source
    theorem ConNF.Sublitter.fst_eq_of_mem [ConNF.Params] {S : ConNF.Sublitter} {a : ConNF.Atom} (h : a ∈ S) :
    a.1 = S.litter
    source
    theorem ConNF.Sublitter.mem_litterSet_of_mem [ConNF.Params] {S : ConNF.Sublitter} {a : ConNF.Atom} (h : a ∈ S) :
    a ∈ ConNF.litterSet S.litter
    source
    @[simp]
    theorem ConNF.Sublitter.mem_mk [ConNF.Params] {a : ConNF.Atom} {L : ConNF.Litter} {S : Set ConNF.Atom} {subset : S ⊆ ConNF.litterSet L} {diff_small : ConNF.Small (ConNF.litterSet L \ S)} :
    a ∈ { litter := L, carrier := S, subset := subset, diff_small := diff_small } ↔ a ∈ S
    source
    @[simp]
    theorem ConNF.Sublitter.litter_diff_eq [ConNF.Params] (S : ConNF.Sublitter) :
    ↑S \ ConNF.litterSet S.litter = ∅
    source
    theorem ConNF.Sublitter.isNearLitter [ConNF.Params] (S : ConNF.Sublitter) :
    ConNF.IsNearLitter S.litter ↑S
    source
    def ConNF.Sublitter.toNearLitter [ConNF.Params] (S : ConNF.Sublitter) :
    ConNF.NearLitter
    Equations
    • S.toNearLitter = ⟨S.litter, ⟨↑S, ⋯⟩⟩
    Instances For
      source
      @[simp]
      theorem ConNF.Sublitter.toNearLitter_litter [ConNF.Params] (S : ConNF.Sublitter) :
      S.toNearLitter.fst = S.litter
      source
      @[simp]
      theorem ConNF.Sublitter.coe_toNearLitter [ConNF.Params] (S : ConNF.Sublitter) :
      ↑S.toNearLitter = ↑S
      source
      @[simp]
      theorem ConNF.Sublitter.mem_toNearLitter [ConNF.Params] {S : ConNF.Sublitter} (a : ConNF.Atom) :
      a ∈ S.toNearLitter ↔ a ∈ S
      source
      theorem ConNF.Sublitter.isNear_iff [ConNF.Params] {S₁ : ConNF.Sublitter} {S₂ : ConNF.Sublitter} :
      ConNF.IsNear ↑S₁ ↑S₂ ↔ S₁.litter = S₂.litter
      source
      theorem ConNF.Sublitter.inter_nonempty_iff [ConNF.Params] {S₁ : ConNF.Sublitter} {S₂ : ConNF.Sublitter} :
      (↑S₁ ∩ ↑S₂).Nonempty ↔ S₁.litter = S₂.litter
      source
      def ConNF.Litter.toSublitter [ConNF.Params] (L : ConNF.Litter) :
      ConNF.Sublitter
      Equations
      • L.toSublitter = { litter := L, carrier := ConNF.litterSet L, subset := ⋯, diff_small := ⋯ }
      Instances For
        source
        @[simp]
        theorem ConNF.Litter.litter_toSublitter [ConNF.Params] (L : ConNF.Litter) :
        L.toSublitter.litter = L
        source
        @[simp]
        theorem ConNF.Litter.coe_toSublitter [ConNF.Params] (L : ConNF.Litter) :
        ↑L.toSublitter = ConNF.litterSet L
        source
        noncomputable def ConNF.Sublitter.equivκ [ConNF.Params] (S : ConNF.Sublitter) :
        ↥S ≃ ConNF.κ
        Equations
        • S.equivκ = ⋯.some
        Instances For
          source
          noncomputable def ConNF.Sublitter.equiv [ConNF.Params] (S : ConNF.Sublitter) (T : ConNF.Sublitter) :
          ↥S ≃ ↥T

          There is an equivalence between any two sublitters.

          Equations
          • S.equiv T = S.equivκ.trans T.equivκ.symm
          Instances For
            source
            @[simp]
            theorem ConNF.Sublitter.equiv_apply_mem [ConNF.Params] {S : ConNF.Sublitter} {T : ConNF.Sublitter} (a : ↥S) :
            ↑((S.equiv T) a) ∈ T
            source
            @[simp]
            theorem ConNF.Sublitter.equiv_symm_apply_mem [ConNF.Params] {S : ConNF.Sublitter} {T : ConNF.Sublitter} (a : ↥T) :
            ↑((S.equiv T).symm a) ∈ S
            source
            @[simp]
            theorem ConNF.Sublitter.equiv_apply_fst_eq [ConNF.Params] {S : ConNF.Sublitter} {T : ConNF.Sublitter} (a : ↥S) :
            (↑((S.equiv T) a)).1 = T.litter
            source
            @[simp]
            theorem ConNF.Sublitter.equiv_symm_apply_fst_eq [ConNF.Params] {S : ConNF.Sublitter} {T : ConNF.Sublitter} (a : ↥T) :
            (↑((S.equiv T).symm a)).1 = S.litter
            source
            theorem ConNF.Sublitter.equiv_congr_left [ConNF.Params] {S : ConNF.Sublitter} {T : ConNF.Sublitter} {U : ConNF.Sublitter} (h : S = T) (a : ↥S) :
            ↑((S.equiv U) a) = ↑((T.equiv U) ⟨↑a, ⋯⟩)
            source
            theorem ConNF.Sublitter.equiv_congr_right [ConNF.Params] {S : ConNF.Sublitter} {T : ConNF.Sublitter} {U : ConNF.Sublitter} (h : T = U) (a : ↥S) :
            ↑((S.equiv T) a) = ↑((S.equiv U) a)