Я новичок в lean - prover, и я пытаюсь найти примеры из онлайн-учебника .
Я застрял в этом примере, и мне нужно доказать, что "false подразумевает"д "или что-то в этом роде. Мой код:
variables p q : Prop
example : ¬ p → (p → q) :=
assume h : ¬ p,
assume hp : p,
--have hnpq : ¬ p ∨ q, from or.inl h,
have hf : false, from h hp,
--show q, from hf
sorry
Я не думаю, что определение hnpq может помочь, потому что это доказательство является частью (¬ p ∨ q) → (p → q). В теории множеств я думаю, что ложь подразумевает все.
Есть предложения или мысли?