find?_ofFn_eq_some_of_injective — Mathlib

English

If f is injective, then (ofFn f).find? p = some (f i) iff p (f i) = true and ∀ j < i, ¬(p (f j) = true).

Русский

Если f инъективно отображает Fin n в α, то (ofFn f).find? p = some (f i) эквивалентно p(f(i)) = true и ∀ j < i, ¬(p(f(j)) = true).

LaTeX

$$$ (\\operatorname{List.find}?\\ p\\ (\\operatorname{List.ofFn} f)) = \\text{some } (f i) \\iff p(f(i)) = \\text{true} \\land \\forall j < i, \\neg (p (f j) = \\text{true}) $$$

Lean4

theorem find?_ofFn_eq_some_of_injective {n} {f : Fin n → α} {p : α → Bool} {i : Fin n} (h : Function.Injective f) :
    (ofFn f).find? p = some (f i) ↔ p (f i) = true ∧ ∀ j < i, ¬(p (f j) = true) := by
  simp only [find?_ofFn_eq_some, h.eq_iff, Bool.not_eq_true, exists_eq_left]

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