iSupLift_mk — Mathlib

English

If T is the iSup of K and hx asserts membership of x in T, then iSupLift maps the representative ⟨x, hx⟩ in T to f_i(x).

Русский

Если T есть супремум по K и hx доказывает принадлежность x T, то iSupLift применимо к представителю ⟨x, hx⟩ в T и даёт 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

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