iSupLift_mk — Mathlib

English

If hx ensures that x ∈ T corresponds to an element of K_i, then iSupLift K dir f hf T hT ⟨x, hx⟩ = f_i(x).

Русский

Пусть hx гарантирует, что x ∈ T соответствует элементу из 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 {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
    {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)} {T : Subalgebra R A} {hT : T = iSup K} {i : ι}
    (x : K i) (hx : (x : A) ∈ T) : iSupLift K dir f hf T hT ⟨x, hx⟩ = f i x :=
  by
  dsimp [iSupLift, inclusion]
  rw [Set.iUnionLift_mk]

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