range_inlAlgHom_sup_adjoin_eps — Mathlib

English

The combination of the images of A and the ε-direction generates the whole algebra.

Русский

Образ A и ε-направление порождают всю алгебру.

LaTeX

$$range_inlAlgHom_sup_adjoin_eps: (inlAlgHom R A A).range ⊔ Algebra.adjoin R {ε} = ⊤$$

Lean4

@[simp]
theorem range_inlAlgHom_sup_adjoin_eps : (inlAlgHom R A A).range ⊔ Algebra.adjoin R {ε} = ⊤ :=
  by
  refine top_unique fun x hx => ?_; clear hx
  rw [← x.inl_fst_add_inr_snd_eq, inr_eq_smul_eps, ← inl_mul_eq_smul]
  refine add_mem ?_ (mul_mem ?_ ?_)
  · exact le_sup_left (α := Subalgebra R _) <| Set.mem_range_self x.fst
  · exact le_sup_left (α := Subalgebra R _) <| Set.mem_range_self x.snd
  · refine le_sup_right (α := Subalgebra R _) <| Algebra.subset_adjoin <| Set.mem_singleton ε

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