coe_sigmaSet — Mathlib

English

The underlying function of sigmaSet is the projection to the α-value, i.e., (sigmaSet h) (i, x) = x.

Русский

Базовая функция sigmaSet равна проекции на значение из α, то есть (sigmaSet(h))(i, x) = x.

LaTeX

$$$(\mathrm{sigmaSet}(h) : ((i, s_i) \to α)) = \lambda (i, x), x$$$

Lean4

@[norm_cast]
theorem coe_sigmaSet {s : ι → Set α} (h) : (Function.Embedding.sigmaSet h : ((i : ι) × s i) → α) = fun x ↦ x.2.1 :=
  rfl

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