distinguishability_lifted_from_bool

formal source

  23
  24/-- Any carrier supporting a Boolean predicate with both truth values
  25inherits an object-level distinction. -/
  26theorem distinguishability_lifted_from_bool
  27    {K : Type*} (P : K → Bool)
  28    (hpos : ∃ x : K, P x = true) (hneg : ∃ x : K, P x = false) :
  29    ∃ x y : K, x ≠ y := by
  30  obtain ⟨x, hx⟩ := hpos
  31  obtain ⟨y, hy⟩ := hneg
  32  refine ⟨x, y, ?_⟩
  33  intro hxy
  34  have hfalse : P x = false := by
  35    simpa [hxy] using hy
  36  cases hx.symm.trans hfalse
  37
  38/-- A proposition is never equal to its negation in classical logic. -/
  39theorem prop_ne_not (P : Prop) : P ≠ ¬ P := by
  40  intro h
  41  by_cases hp : P
  42  · have hnp : ¬ P := by
  43      rw [h] at hp
  44      exact hp
  45    exact hnp hp
  46  · have hp' : P := by
  47      rw [h.symm] at hp
  48      exact hp
  49    exact hp hp'
  50
  51/-- The claim that a carrier admits a non-trivial distinction is itself
  52distinguishable from the denial of that claim. -/
  53theorem dist_claim_self_distinguishes (K : Type*) :
  54    (∃ x y : K, x ≠ y) ≠ (¬ ∃ x y : K, x ≠ y) :=
  55  prop_ne_not (∃ x y : K, x ≠ y)
  56