le_union — Mathlib

English

If σ is in a chain c, then σ is below the union of the chain.

Русский

Если σ принадлежит цепи c, то σ ≤ объединение цепи.

LaTeX

$$$\forall \sigma \in c, \sigma \le \bigcup c$$$

Lean4

theorem le_union ⦃σ : Lifts F E K⦄ (hσ : σ ∈ c) : σ ≤ union c hc :=
  have hσ := Set.mem_insert_of_mem ⊥ hσ
  let t (i : ↑(insert ⊥ c)) := i.val.carrier
  ⟨le_iSup t ⟨σ, hσ⟩, fun x ↦ by
    dsimp only [union, AlgHom.comp_apply]
    exact
      Subalgebra.iSupLift_inclusion (K := (toSubalgebra <| t ·)) (i := ⟨σ, hσ⟩) x
        (le_iSup (toSubalgebra <| t ·) ⟨σ, hσ⟩)⟩

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