101theorem locally_regular_cell_connected (L : LocalConfigSpace C) (r : Recognizer C E) 102 (c : C) (h : IsLocallyRegular L r c) : 103 ∃ U ∈ L.N c, IsRecognitionConnected r (ResolutionCell r c ∩ U) := by
proof body
Term-mode proof.
104 obtain ⟨U, hU, hconn⟩ := h 105 use U, hU 106 -- ResolutionCell r c = r.R ⁻¹' {r.R c} by definition of Indistinguishable 107 intro c₁ c₂ h₁ h₂ 108 simp only [ResolutionCell, Set.mem_inter_iff, Set.mem_setOf_eq] at h₁ h₂ 109 -- c₁, c₂ both in preimage of {r.R c} ∩ U 110 have hc₁ : c₁ ∈ r.R ⁻¹' {r.R c} ∩ U := ⟨h₁.1, h₁.2⟩ 111 have hc₂ : c₂ ∈ r.R ⁻¹' {r.R c} ∩ U := ⟨h₂.1, h₂.2⟩ 112 exact hconn c₁ c₂ hc₁ hc₂ 113 114/-- A constant recognizer is locally regular everywhere. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.