assert_defined — Mathlib

English

For any proposition p and a family f : p → Part α, there is a relation asserting that if h ∈ p, and f(h) has a domain, then the asserted element is defined.

Русский

Для любого утверждения p и семейства f : p → Part α существует утверждение о том, что если h ∈ p и f(h) имеет область определения, то утверждённый элемент определён.

LaTeX

$$$\\forall p:\\mathrm{Prop},\\ f:p \\to\\mathrm{Part}\\;\\alpha,\\ h:\\,p,\\; (f\\,h).Dom \\Rightarrow (\\mathrm{assert}\\ p\\ f).Dom$$$

Lean4

theorem assert_defined {p : Prop} {f : p → Part α} : ∀ h : p, (f h).Dom → (assert p f).Dom :=
  Exists.intro

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