pith. machine review for the scientific record. sign in
theorem proved term proof

finite_resolution_cell_finite_events

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  63theorem finite_resolution_cell_finite_events (c : C)
  64    (h : HasFiniteLocalResolution L r c) :
  65    ∃ U ∈ L.N c, ∀ c' ∈ U, r.R c' ∈ r.R '' U ∧ (r.R '' U).Finite := by

proof body

Term-mode proof.

  66  obtain ⟨U, hU, hfin⟩ := h
  67  use U, hU
  68  intro c' hc'
  69  exact ⟨⟨c', hc', rfl⟩, hfin⟩
  70
  71/-! ## Discrete Local Recognition Geometry -/
  72
  73/-- A recognition geometry is locally discrete if events are finite everywhere -/

depends on (12)

Lean names referenced from this declaration's body.