theorem
proved
tactic proof
chart_exists_implies
show as:
view Lean formalization →
formal statement (Lean)
193theorem chart_exists_implies (φ : RecognitionChart L r n)
194 (c : C) (hc : c ∈ φ.domain)
195 (h_no_chart : ∀ (c : C) (U : Set C), U ∈ L.N c →
196 Set.Infinite U → (r.R '' U).Finite → (n : ℕ) →
197 ¬∃ φ : RecognitionChart L r n, φ.domain = U) :
198 Set.Finite φ.domain ∨ Set.Infinite (r.R '' φ.domain) := by
proof body
Tactic-mode proof.
199 by_contra h
200 push_neg at h
201 obtain ⟨hinf, hfin⟩ := h
202 obtain ⟨c', hc'⟩ := φ.domain_is_nbhd
203 -- Apply finite_resolution_no_chart
204 exact absurd ⟨φ, rfl⟩ (h_no_chart c' φ.domain hc' hinf hfin n)
205
206/-! ## Smooth Structure Emergence -/
207
208/-- A recognition geometry is **smooth** if it admits a smooth atlas.
209
210 This is the bridge to classical differential geometry: when recognition
211 structure is "rich enough," the quotient space looks like a manifold. -/