iUnionLift_of_mem — Mathlib

English

For any x in T and any i with x ∈ S_i, iUnionLift S f hf T hT x equals f_i ⟨x, hx⟩. In particular, the value is determined by any one index i containing x.

Русский

Для любого x в T и любого i, где x ∈ S_i, iUnionLift S f hf T hT x равно f_i ⟨x, hx⟩. Значение определяется любым индексом i, содержащим x.

LaTeX

$$$\forall x\in T,\; \forall i\in ι\, (x\in S_i)\Rightarrow iUnionLift S f hf T hT x = f_i\langle x, hx\rangle.$$$

Lean4

theorem iUnionLift_of_mem (x : T) {i : ι} (hx : (x : α) ∈ S i) : iUnionLift S f hf T hT x = f i ⟨x, hx⟩ := by
  obtain ⟨x, hx⟩ := x; exact hf _ _ _ _ _

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