mem_fill_iff — Mathlib

English

Characterization of membership in a filled Sym term: a is either equal to the filled value with nonzero copies or comes from the tail.

Русский

Характеристика членства в заполненном Sym-терме: элемент либо равен заполняемой величине с ненулевым количеством копий, либо принадлежит хвосту.

LaTeX

$$$ a \\in \\mathrm{fill}\\ b\\ i\\ s \\iff (i \\neq 0 \\land a = b) \\lor (a \\in s) $$$

Lean4

theorem mem_fill_iff {a b : α} {i : Fin (n + 1)} {s : Sym α (n - i)} :
    a ∈ Sym.fill b i s ↔ (i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s := by rw [fill, mem_cast, mem_append_iff, or_comm, mem_replicate]

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