cast — Mathlib

English

Given s ∈ X.S with hd: s.dim = d, there is a cast s ∈ X.S with dim exactly d and simplex equal to the cast of s.simplex along hd.

Русский

Для s ∈ X.S с hd: s.dim = d существует элемент cast(s) ∈ X.S с dim ровно d и simplex, равным преобразованию s.simplex по hd.

LaTeX

$$$\text{cast}(s) := \langle d, \operatorname{cast}(h)(s.simplex) \rangle$$$

Lean4

/-- When `s : X.S` is such that `s.dim = d`, this is a term
that is equal to `s`, but whose dimension if definitionally equal to `d`. -/
@[simps dim]
def cast : X.S where
  dim := d
  simplex := _root_.cast (by simp only [hd]) s.simplex

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