get_ofNat' — Mathlib

English

For x ∈ ℕ with AtLeastTwo and h : (ofNat(x) : PartENat).Dom, Part.get (ofNat(x) : PartENat) h = ofNat(x).

Русский

Для x ∈ ℕ с AtLeastTwo и h : (ofNat(x) : PartENat).Dom, Part.get (ofNat(x) : PartENat) h = ofNat(x).

LaTeX

$$@[simp] get_ofNat' (x : ℕ) [x.AtLeastTwo] (h : (ofNat(x) : PartENat).Dom) : Part.get (ofNat(x) : PartENat) h = ofNat(x)$$

Lean4

@[simp]
theorem get_ofNat' (x : ℕ) [x.AtLeastTwo] (h : (ofNat(x) : PartENat).Dom) :
    Part.get (ofNat(x) : PartENat) h = ofNat(x) :=
  get_natCast' x h

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