Forall — Mathlib

English

For any predicate P on m×n matrices, Forall P encodes the universal quantification over all entries of matrices in a way that is definitional equal to ∀X, P(X).

Русский

Для любых предикатов P над матрицами размера m×n Forall P кодирует тот же квантор, что и ∀X, P(X).

LaTeX

$$$\\text{Forall }P \\;\\leftrightarrow\\; \\forall X, P(X)$$$

Lean4

/-- `∀` with better defeq for `∀ x : Matrix (Fin m) (Fin n) α, P x`. -/
def Forall : ∀ {m n} (_ : Matrix (Fin m) (Fin n) α → Prop), Prop
  | 0, _, P => P (of ![])
  | _ + 1, _, P => FinVec.Forall fun r => Forall fun A => P (of (Matrix.vecCons r A))

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