BarycentricIncidence.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Codimension-one incidence in the actual face-chain subdivision

Completions of a flag are counted by inserting its unique missing rank. An interior missing rank has two completions. A missing top rank inherits the incidence count of the greatest old face.

theorem OAI.Tingley.FiniteComplex.chain_insert_iff line 21
def OAI.Tingley.FiniteComplex.insertionVertices line 41
theorem OAI.Tingley.FiniteComplex.mem_insertionVertices line 46
theorem OAI.Tingley.FiniteComplex.incidentTop_sd_eq_image_insert line 51
theorem OAI.Tingley.FiniteComplex.incidentTop_sd_card_eq_insertionVertices line 71
theorem OAI.Tingley.FiniteComplex.rank_ne_of_missing line 80
theorem OAI.Tingley.FiniteComplex.missing_rank_unique line 87
theorem OAI.Tingley.FiniteComplex.insertionVertices_card_eq_missing line 98

theorem OAI.Tingley.FiniteComplex.card_insertionVertices_eq_sdiff line 117

Source documentation

Count possible inserted old faces between two consecutive retained ranks.

theorem card_insertionVertices_eq_sdiff {c : Finset (FaceVertex K)}
    {L U : Finset V} (hU : U ∈ K.faces) (hLU : L ⊆ U)
    (hmem : ∀ a : FaceVertex K, a ∈ K.insertionVertices c ↔
      L ⊆ a.val ∧ a.val ⊆ U ∧ a.val.card = L.card + 1) :
    (K.insertionVertices c).card = (U \ L).card := by
…

Mentions: OAI.Tingley.FiniteComplex.FaceVertex

theorem OAI.Tingley.FiniteComplex.incidentTop_sd_card_two_of_missing_rank line 152

Source documentation

An omitted rank strictly below the top has exactly two completions.

theorem incidentTop_sd_card_two_of_missing_rank {m r : ℕ} (hK : K.CardBound m)
    {c : Finset (FaceVertex K)} (hc : c ∈ K.sd.codimFaces m)
    (hr₁ : 1 ≤ r) (hrm : r ≤ m)
    (hr : K.ranks c = (Finset.Icc 1 (m + 1)).erase r) :
    (K.sd.incidentTop m c).card = 2 := by
…

Mentions: OAI.Tingley.FiniteComplex.FaceVertex

theorem OAI.Tingley.FiniteComplex.incidentTop_sd_card_eq_of_missing_top line 221

Source documentation

If the omitted rank is the top rank, completions are exactly the old top faces containing the retained rank-m face.

theorem incidentTop_sd_card_eq_of_missing_top {m : ℕ} (hK : K.CardBound m)
    {c : Finset (FaceVertex K)} (hc : c ∈ K.sd.codimFaces m)
    (hr : K.ranks c = (Finset.Icc 1 (m + 1)).erase (m + 1))
    {T : FaceVertex K} (hTc : T ∈ c) (hTcard : T.val.card = m) :
    (K.sd.incidentTop m c).card = (K.incidentTop m T.val).card := by
…

Mentions: OAI.Tingley.FiniteComplex.FaceVertex

theorem OAI.Tingley.FiniteComplex.incidentTop_sd_missing_top_data line 265

theorem OAI.Tingley.FiniteComplex.incidentTop_sd_cases line 283

Source documentation

The complete positive-dimensional codimension-one alternative. The first case also records a retained old top face for transferring carrier information.

theorem incidentTop_sd_cases {m : ℕ} (hm : 0 < m) (hK : K.CardBound m)
    {c : Finset (FaceVertex K)} (hc : c ∈ K.sd.codimFaces m) :
    ((K.sd.incidentTop m c).card = 2 ∧
      ∃ T ∈ c, T.val.card = m + 1 ∧ ∀ b ∈ c, b.val ⊆ T.val) ∨
    (∃ T ∈ c, T.val.card = m ∧ (∀ b ∈ c, b.val ⊆ T.val) ∧
      (K.sd.incidentTop m c).card = (K.incidentTop m T.val).card) := by
…

Mentions: OAI.Tingley.FiniteComplex.FaceVertex