iUnionLift_inclusion — Mathlib

English

If each S_i is contained in T and we identify S_i with its image inside T, then iUnionLift evaluates to f_i on elements of S_i, i.e., iUnionLift S f hf T hT (inclusion h x) = f_i x.

Русский

Если каждый S_i содержится в T и мы идентифицируем S_i с её образом в T, то iUnionLift принимает значение f_i на элементах S_i: iUnionLift ... (inclusion h x) = f_i x.

LaTeX

$$$\forall i\in ι,\; \forall x\in S_i:\ h:\ S_i \subseteq T \Rightarrow iUnionLift S f hf T hT (\mathrm{inclusion}\; h\; x) = f_i(x).$$$

Lean4

theorem iUnionLift_inclusion {i : ι} (x : S i) (h : S i ⊆ T) : iUnionLift S f hf T hT (Set.inclusion h x) = f i x :=
  iUnionLift_mk x _

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