toSubspace — Mathlib

English

Given a line l in η → α, construct a subspace in η × ι → α by pairing the i-coordinate with η.

Русский

Задано линию l в η → α, строится подпространство в η × ι → α, соединяя координату i с η.

LaTeX

$$$\\mathrm{toSubspace}(l):\\ Subspace\\ η\\ α\\ (ι\\times η)$ with $\\mathrm{idxFun}(i,e) = (l.idxFun i).\\elim(\\mathrm{inr}\\,e) (\\lambda f.\\mathrm{inl}(f,e))$$$

Lean4

/-- Consider a line in `ι → η → α` as a `η`-dimensional subspace in `ι × η → α`. -/
def toSubspace (l : Line (η → α) ι) : Subspace η α (ι × η)
    where
  idxFun ie := (l.idxFun ie.1).elim (.inr ie.2) (fun f ↦ .inl <| f ie.2)
  proper
    e :=
    let ⟨i, hi⟩ := l.proper;
    ⟨(i, e), by simp [hi]⟩

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