iUnionLift_mk — Mathlib

English

If x ∈ S_i, and x is viewed inside the glued union via the natural inclusion, then iUnionLift assigns to x the original value f_i(x).

Русский

Если x принадлежит S_i и рассматривается как элемент объединения через естественное вложение, то iUnionLift сопоставляет x исходное значение f_i(x).

LaTeX

$$$\forall i\in ι,\; \forall x\in S_i:\ \text{hx}: (x\,:\,\alpha)\in T \ \Longrightarrow\ iUnionLift S f hf T hT \langle x, hx\rangle = f_i(x).$$$

Lean4

@[simp]
theorem iUnionLift_mk {i : ι} (x : S i) (hx : (x : α) ∈ T) : iUnionLift S f hf T hT ⟨x, hx⟩ = f i x :=
  hf _ i x _ _

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