82noncomputable def chartOnQuotient (φ : RecognitionChart L r n) : 83 {q : RecognitionQuotient r // ∃ c ∈ φ.domain, recognitionQuotientMk r c = q} → 84 (Fin n → ℝ) :=
proof body
Definition body.
85 fun ⟨_, hq⟩ => 86 let c := hq.choose 87 let hc : c ∈ φ.domain ∧ recognitionQuotientMk r c = _ := hq.choose_spec 88 φ.toFun ⟨c, hc.1⟩ 89 90/-- The chart on quotient is well-defined (independent of representative) -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.