coe_add_get — Mathlib

English

For x ∈ ℕ and y ∈ PartENat, if the sum (x : PartENat) + y is defined, then its get equals x plus y.get with the appropriate projection.

Русский

Для x ∈ ℕ и y ∈ PartENat, если сумма (x : PartENat) + y определима, то её значение равно x плюс значение y.

LaTeX

$$$\\\\forall {x : \\\\mathbb{N}} {y : \\\\mathrm{PartENat}} (h : ((x : \\\\mathrm{PartENat}) + y).\\\\Dom),\\\\; get ((x : \\\\mathrm{PartENat}) + y) h = x + get y h.2$$$

Lean4

theorem coe_add_get {x : ℕ} {y : PartENat} (h : ((x : PartENat) + y).Dom) :
    get ((x : PartENat) + y) h = x + get y h.2 := by rfl

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