129theorem nontrivial_recognition_forces_interface (K : Type*) : 130 NontrivialRecognition K → 131 ∃ (I : PrimitiveInterface K) (x y : K), 132 equalityDistinction K x y ∧ Separates I x y := by
proof body
Term-mode proof.
133 intro h 134 rcases h with ⟨x, y, hxy⟩ 135 exact ⟨pointInterface x, x, y, hxy, pointInterface_separates hxy⟩ 136 137/-- Same theorem under the observer name: non-trivial recognition forces a 138primitive observer. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.