exists_prop_of_false

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#exists_prop_of_false

English

If p is false, then there is no x with p x and q x; i.e., ¬p → ¬∃ h' : p, q h'.

Русский

Если p ложно, то не существует x, для которого p(x) и q(x).

LaTeX

$$$(\neg p) \Rightarrow \neg(\exists h': p(h') , q(h'))$$$

Lean4

theorem exists_prop_of_false {p : Prop} {q : p → Prop} : ¬p → ¬∃ h' : p, q h' :=
  mt Exists.fst

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

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

Разделы

Аффилиация

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