rfind_zero_none — Mathlib

English

Let p: N ⇀ Bool be a partial function. If p(0) is undefined, then rfind p is undefined.

Русский

Пусть p: ℕ ⇀ Bool — частичная функция. Если p(0) неопределена, то rfind p неопределён.

LaTeX

$$$\text{Let } p: \mathbb{N} \rightharpoonup \mathsf{Bool}.\; p(0)=\mathrm{Part.none} \Rightarrow \mathrm{rfind}(p)=\mathrm{Part.none}.$$$

Lean4

theorem rfind_zero_none (p : ℕ →. Bool) (p0 : p 0 = Part.none) : rfind p = Part.none :=
  eq_none_iff.2 fun _ h =>
    let ⟨_, _, h₂⟩ := rfind_dom'.1 h.fst
    (p0 ▸ h₂ (zero_le _) : (@Part.none Bool).Dom)

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