fact non-instances — Mathlib

English

Fact p is equivalent to p itself; a proposition is true iff it is provable as a Fact.

Русский

Fact p эквивалентно самому p; утверждение истинно тогда и только тогда, когда его можно доказать как факт.

LaTeX

$$$ \\mathrm{Fact}\, p \\;\\iff\\; p. $$$

Lean4

/-- In most cases, we should not have global instances of `Fact`; typeclass search is not an
advanced proof search engine, and adding any such instance has the potential to cause
slowdowns everywhere. We instead declare them as lemmata and make them local instances as required.
-/
def «fact non-instances» : LibraryNote✝ :=
  ()

Похожие утверждения