not_exists

Mathlib.Tactic.Push

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Push.not_exists

Lean4

@[push]
theorem not_exists : (¬∃ x, s x) ↔ (∀ x, binderNameHint x s <| ¬s x) :=
  _root_.not_exists

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru