assert_pos — Mathlib

English

Given a Prop p and a function f : p → Part α, Part.assert p f equals f h for any proof h of p.

Русский

Для данного утверждения p и функции f : p → Part α, Part.assert p f равно f h для любого доказательства h p.

LaTeX

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

Lean4

theorem assert_pos {p : Prop} {f : p → Part α} (h : p) : assert p f = f h :=
  by
  dsimp [assert]
  cases h' : f h
  simp only [h', mk.injEq, h, exists_prop_of_true, true_and]
  apply Function.hfunext
  · simp only [h, h', exists_prop_of_true]
  · simp

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