findMin'_all — Mathlib

English

For any predicate P, if All P t holds and P x holds, then P holds for findMin' t x.

Русский

Для любого предиката P, если All P t верно и P x верно, тогда P выполняется для findMin' t x.

LaTeX

$${P : α → Prop} \; ∀ t x,\; All P t → P x → P (findMin' t x)$$

Lean4

@[elab_as_elim]
theorem findMin'_all {P : α → Prop} : ∀ (t) (x : α), All P t → P x → P (findMin' t x)
  | nil, _x, _, hx => hx
  | node _ ll lx _, _, ⟨h₁, h₂, _⟩, _ => findMin'_all ll lx h₁ h₂

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