natCast_get — Mathlib

English

If x lies in its domain, converting its get back to PartENat yields x.

Русский

Если x находится в своей области определения, преобразование его значения обратно в PartENat даёт x.

LaTeX

$$$\\text{theorem } natCastGet: \\forall {x : \\mathrm{PartENat}} (h : x.\\\\Dom), (x.get h : \\mathrm{PartENat}) = x$$$

Lean4

@[simp]
theorem natCast_get {x : PartENat} (h : x.Dom) : (x.get h : PartENat) = x := by
  exact Part.ext' (iff_of_true trivial h) fun _ _ => rfl

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