horizontal_apply — Mathlib

English

For l: Line α ι and v: ι'→α, l.horizontal v x = Sum.elim (l x) v.

Русский

Для l: Line α ι и v: ι'→α, l.horizontal v x = Sum.elim (l x) v.

LaTeX

$$$\\forall l:\\ Line\\alpha\\ ι,\\ \\forall v:\\iota'\\to\\alpha,\\forall x:\\alpha,\\ l.horizontal\\ v\\ x = Sum.elim (l\\,x)\\ v.$$$

Lean4

@[simp]
theorem horizontal_apply {α ι ι'} (l : Line α ι) (v : ι' → α) (x : α) : l.horizontal v x = Sum.elim (l x) v :=
  by
  funext i
  cases i <;> rfl

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