iSupLift_mk — Mathlib

English

If i ∈ ι and hx ∈ K i, then iSupLift K dir f hf T hT ⟨x, hx⟩ = f i x.

Русский

Если i принадлежит индексной множеству и hx ∈ K_i, то iSupLift(K,dir,f,hf,T,hT)(⟨x,hx⟩) = f_i(x).

LaTeX

$$$iSupLift\\ K dir f hf T hT \\langle x, hx \\rangle = f i x$$$

Lean4

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

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