English
Let α, β, γ be types and C a predicate on triples of vectors of the same length. Suppose nil : C nil nil nil and cons : ∀ {n a b c} {x : Vector α n} {y} {z}, C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z). Then for any u, v, w of the same length, C u v w.
Русский
Пусть α, β, γ — множества и C предикат на тройке векторов одинаковой длины. Пусть nil : C nil nil nil и cons : ∀ {n a b c} {x : Vector α n} {y} {z}, C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z). Тогда для любых u, v, w той же длины выполняется C u v w.
LaTeX
$$$ C\\; u\\; v\\; w \\\\text{ при условии: } nil : C\\, nil\\, nil\\, nil\\; и\\; cons : ∀ {n a b c} {x : Vector α n} {y : Vector β n} {z : Vector γ n}, C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z) \\Rightarrow C\\, u\\, v\\, w $$$
Lean4
/-- Define `C u v w` by induction on a triplet of vectors
`u : Vector α n`, `v : Vector β n`, and `w : Vector γ b`. -/
@[elab_as_elim]
def inductionOn₃ {C : ∀ {n}, Vector α n → Vector β n → Vector γ n → Sort*} (u : Vector α n) (v : Vector β n)
(w : Vector γ n) (nil : C nil nil nil)
(cons : ∀ {n a b c} {x : Vector α n} {y z}, C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)) : C u v w := by
induction n with
| zero =>
rcases u with ⟨_ | ⟨-, -⟩, - | -⟩
rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
exact nil
| succ n ih =>
rcases u with ⟨_ | ⟨a, u⟩, u_property⟩
cases u_property
rcases v with ⟨_ | ⟨b, v⟩, v_property⟩
cases v_property
rcases w with ⟨_ | ⟨c, w⟩, w_property⟩
cases w_property
apply
@cons n _ _ _ ⟨u, (add_left_inj 1).mp u_property⟩ ⟨v, (add_left_inj 1).mp v_property⟩
⟨w, (add_left_inj 1).mp w_property⟩
apply ih
