iSupLift_of_mem — Mathlib

English

Let x ∈ T be such that (x:A) ∈ K_i (i.e., x comes from K_i). Then iSupLift K dir f hf T hT x = f_i ⟨x, hx⟩.

Русский

Пусть x ∈ T и (x:A) принадлежит K_i, то есть x проистекает из K_i. Тогда iSupLift K dir f hf T hT 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 {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 : T) (hx : (x : A) ∈ K i) : iSupLift K dir f hf T hT x = f i ⟨x, hx⟩ :=
  by
  dsimp [iSupLift, inclusion]
  rw [Set.iUnionLift_of_mem]

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