pith. machine review for the scientific record. sign in
theorem proved tactic proof

prop_ne_not

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  39theorem prop_ne_not (P : Prop) : P ≠ ¬ P := by

proof body

Tactic-mode proof.

  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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.