const_iff_true — Mathlib

English

For any i and x in α i and any proposition p, the value read from a constant-predicate vector at position i is equivalent to p.

Русский

Для любого i и x ∈ α i и любого предиката p значение константного векторного предиката на позиции i эквивалентно p.

LaTeX

$$$\\operatorname{ofRepeat}(\\mathrm{TypeVec}.const\, p\, \\alpha\, i\, x) \\iff p.$$$

Lean4

theorem const_iff_true {α : TypeVec n} {i x p} : ofRepeat (TypeVec.const p α i x) ↔ p := by
  induction i with
  | fz => rfl
  | fs _ ih =>
    rw [TypeVec.const]
    exact ih

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