theorem
proved
term proof
locally_discrete_finite_classes
show as:
view Lean formalization →
formal statement (Lean)
79theorem locally_discrete_finite_classes
80 (h : IsLocallyDiscrete L r) (c : C) :
81 ∃ U ∈ L.N c, (r.R '' U).Finite :=
proof body
Term-mode proof.
82 h c
83
84/-! ## No Continuous Injection Theorem -/
85
86/-- **Key Insight**: If a neighborhood has infinite configurations but finite
87 events, then the recognizer cannot be injective on that neighborhood.
88
89 This explains why discrete recognition geometry fundamentally differs
90 from continuous Euclidean geometry. -/