assert_neg — Mathlib

English

If ¬p, then Part.assert p f = none.

Русский

Если не выполняется p, то Part.assert p f = none.

LaTeX

$$$ \forall {p} {f : p \rightarrow \mathrm{Part}(\alpha)} (h : \neg p), \mathrm{Part.assert}(p,f) = \mathrm{none}$$$

Lean4

theorem assert_neg {p : Prop} {f : p → Part α} (h : ¬p) : assert p f = none :=
  by
  dsimp [assert, none]; congr
  · simp only [h, not_false_iff, exists_prop_of_false]
  · apply Function.hfunext
    · simp only [h, not_false_iff, exists_prop_of_false]
    simp at *

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