finite_resolution_not_injective

formal source

 105
 106/-- Corollary: Finite local resolution at c implies non-injectivity
 107    on any infinite neighborhood containing c -/
 108theorem finite_resolution_not_injective (c : C)
 109    (h : HasFiniteLocalResolution L r c)
 110    (hinf : ∀ U ∈ L.N c, Set.Infinite U) :
 111    ∃ U ∈ L.N c, ¬Function.Injective (r.R ∘ Subtype.val : U → E) := by
 112  obtain ⟨U, hU, hfin⟩ := h
 113  exact ⟨U, hU, no_injection_on_infinite_finite L r c U hU (hinf U hU) hfin⟩
 114
 115/-! ## Resolution Count -/
 116
 117/-- Count of distinct events in a neighborhood (when finite) -/
 118noncomputable def eventCount (U : Set C) (hfin : (r.R '' U).Finite) : ℕ :=
 119  hfin.toFinset.card
 120
 121/-- Event count is positive when the neighborhood is nonempty -/
 122theorem eventCount_pos (c : C) (U : Set C) (hU : U ∈ L.N c)
 123    (hfin : (r.R '' U).Finite) :
 124    0 < eventCount r U hfin := by
 125  unfold eventCount
 126  have hc : c ∈ U := L.mem_of_mem_N c U hU
 127  have hne : (r.R '' U).Nonempty := ⟨r.R c, ⟨c, hc, rfl⟩⟩
 128  exact Finset.card_pos.mpr ((Set.Finite.toFinset_nonempty hfin).mpr hne)
 129
 130/-! ## Resolution Bound -/
 131
 132/-- Given a finite set of events, count them -/
 133noncomputable def eventCountFinite (S : Set E) (hfin : S.Finite) : ℕ :=
 134  hfin.toFinset.card
 135
 136/-- Event count is positive for nonempty sets -/
 137theorem eventCountFinite_pos (S : Set E) (hfin : S.Finite) (hne : S.Nonempty) :
 138    0 < eventCountFinite S hfin := by