New file

In this file...

Main declarations

• ConNF.foo: Something new.

structure ConNF.InflexiblePath [Params] (β : TypeIndex) : Type u

• γ : Λ
• δ : TypeIndex
• ε : Λ
• hδ : self.δ < ↑self.γ
• hε : ↑self.ε < ↑self.γ
• hδε : self.δ ≠ ↑self.ε
• A : β ↝ ↑self.γ

theorem ConNF.InflexiblePath.ext {inst✝ : Params} {β : TypeIndex} {x y : InflexiblePath β} (γ : x.γ = y.γ) (δ : x.δ = y.δ) (ε : x.ε = y.ε) (A : HEq x.A y.A) : x = y

instance ConNF.instCoderivativeInflexiblePath [Params] {β β' : TypeIndex} : Coderivative (InflexiblePath β) (InflexiblePath β') β' β

Equations

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

@[simp]

theorem ConNF.InflexiblePath.coderiv_A [Params] {β β' : TypeIndex} (P : InflexiblePath β) (B : β' ↝ β) : (P ⇗ B).A = B ⇘ P.A

instance ConNF.instLeLevelSomeΛγ [Params] {β : TypeIndex} [Level] [LeLevel β] (P : InflexiblePath β) : LeLevel ↑P.γ

instance ConNF.instLtLevelδOfLeLevel [Params] {β : TypeIndex} [Level] [LeLevel β] (P : InflexiblePath β) : LtLevel P.δ

instance ConNF.instLtLevelSomeΛεOfLeLevel [Params] {β : TypeIndex} [Level] [LeLevel β] (P : InflexiblePath β) : LtLevel ↑P.ε

def ConNF.Inflexible [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (A : β ↝ ⊥) (L : Litter) : Prop

Equations

• ConNF.Inflexible A L = ∃ (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ), A = P.A ↘ ⋯ ↘. ∧ L = ConNF.fuzz ⋯ t

theorem ConNF.inflexible_iff [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (A : β ↝ ⊥) (L : Litter) : Inflexible A L ↔ ∃ (P : InflexiblePath β) (t : Tangle P.δ), A = P.A ↘ ⋯ ↘. ∧ L = fuzz ⋯ t

theorem ConNF.not_inflexible_iff [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (A : β ↝ ⊥) (L : Litter) : ¬Inflexible A L ↔ ∀ (P : InflexiblePath β) (t : Tangle P.δ), A = P.A ↘ ⋯ ↘. → L ≠ fuzz ⋯ t

theorem ConNF.inflexible_deriv [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] {A : β ↝ ⊥} {L : Litter} (h : Inflexible A L) {β' : TypeIndex} [LeLevel β'] (B : β' ↝ β) : Inflexible (B ⇘ A) L

theorem ConNF.inflexible_cases [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (A : β ↝ ⊥) (L : Litter) : (∃ (P : InflexiblePath β) (t : Tangle P.δ), A = P.A ↘ ⋯ ↘. ∧ L = fuzz ⋯ t) ∨ ¬Inflexible A L

theorem ConNF.inflexiblePath_subsingleton [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] {A : β ↝ ⊥} {L : Litter} {P₁ P₂ : InflexiblePath β} {t₁ : Tangle P₁.δ} {t₂ : Tangle P₂.δ} (hP₁ : A = P₁.A ↘ ⋯ ↘.) (hP₂ : A = P₂.A ↘ ⋯ ↘.) (ht₁ : L = fuzz ⋯ t₁) (ht₂ : L = fuzz ⋯ t₂) : P₁ = P₂

def ConNF.inflexiblePathEmbedding [Params] {β : TypeIndex} : InflexiblePath β ↪ ↑(Set.Iic β) × ↑(Set.Iic β) × (γ : TypeIndex) × β ↝ γ

Equations

• ConNF.inflexiblePathEmbedding = { toFun := fun (P : ConNF.InflexiblePath β) => (⟨P.δ, ⋯⟩, ⟨↑P.ε, ⋯⟩, ⟨↑P.γ, P.A⟩), inj' := ⋯ }

theorem ConNF.card_inflexiblePath_lt [Params] (β : TypeIndex) : Cardinal.mk (InflexiblePath β) < (Cardinal.mk μ).ord.cof