English
For a set S of Subalgebras with nonempty S, the supremum subalgebra maps to a supremum of subsemirings: (sSup S).toSubsemiring = sSup (toSubsemiring '' S).
Русский
Для множества подпалгебр S с непустым множеством, верхняя граница сопоставляется верхнему пределу подполей: (sSup S).toSubsemiring = sSup (toSubsemiring '' S).
LaTeX
$$$(sSup S).toSubsemiring = sSup( toSubsemiring '' S )$$
Lean4
@[simp]
theorem sSup_toSubsemiring (S : Set (Subalgebra R A)) (hS : S.Nonempty) :
(sSup S).toSubsemiring = sSup (toSubsemiring '' S) :=
by
have h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S) :=
by
rw [Set.image_image]
congr! with x
exact x.toSubsemiring.closure_eq.symm
rw [h, sSup_image, ← Subsemiring.closure_sUnion, sSup_def, adjoin_toSubsemiring]
congr 1
rw [Set.union_eq_right]
rintro _ ⟨x, rfl⟩
obtain ⟨y, hy⟩ := hS
simp only [Set.mem_sUnion, Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe]
exact ⟨y, hy, algebraMap_mem y x⟩
