find_congr' — Mathlib

English

A variant characterization of equality of Nat.find in terms of p and a bound on smaller values (auxiliary form).

Русский

Вариант характеристик равенства Nat.find через p и ограничение на меньшие значения (вспомогательная форма).

LaTeX

$$$\\text{(auxiliary form of find_eq_iff)} \\ $$$$

Lean4

/-- A weak version of `Nat.find_congr`, requiring `p = q` everywhere. -/
theorem find_congr' [DecidablePred q] {hp : ∃ n, p n} {hq : ∃ n, q n} (hpq : ∀ {n}, p n ↔ q n) :
    Nat.find hp = Nat.find hq :=
  let ⟨_, hp⟩ := hp;
  find_congr hp fun _ _ ↦ hpq

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