iSupLift_of_mem — Mathlib

English

In the same setting, for x ∈ T coming from K_i with hx its K_i-membership, iSupLift x equals f_i of the corresponding representative.

Русский

В той же конфигурации для x ∈ T, полученного из K_i с hx принадлежности, iSupLift x равно f_i(⟨x, hx⟩).

LaTeX

$$$iSupLift(K, dir, f, hf, T, hT)(x) = f_i(\langle x, hx\rangle)$$$

Lean4

theorem iSupLift_of_mem {i : ι} (x : T) (hx : (x : A) ∈ K i) : iSupLift K dir f hf T hT x = f i ⟨x, hx⟩ :=
  by
  subst hT
  dsimp [iSupLift]
  apply Set.iUnionLift_of_mem

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