64theorem quotientEventMap_injective : 65 Function.Injective (quotientEventMap r) := by
proof body
Term-mode proof.
66 intro q₁ q₂ h 67 obtain ⟨c₁, hc₁⟩ := Quotient.exists_rep q₁ 68 obtain ⟨c₂, hc₂⟩ := Quotient.exists_rep q₂ 69 simp only [← hc₁, ← hc₂] at h ⊢ 70 -- h : quotientEventMap r ⟦c₁⟧ = quotientEventMap r ⟦c₂⟧ 71 -- which means r.R c₁ = r.R c₂ 72 apply Quotient.sound 73 exact h 74 75/-- The quotient is isomorphic to the image of R -/
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.