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 ε