English
For Subalgebras S and T, the infimum of their subsemirings equals the subsemiring of the infimum: (S ⊓ T).toSubsemiring = S.toSubsemiring ⊓ T.toSubsemiring.
Русский
Для подпалгебр S и T пересечение их соответствующих подполей подсемерав равняется пересечению самих подсемирий: (S ⊓ T).toSubsemiring = S.toSubsemiring ⊓ T.toSubsemiring.
LaTeX
$$$(S \cap T).toSubsemiring = S.toSubsemiring \cap T.toSubsemiring$$$
Lean4
@[simp]
theorem sup_toSubsemiring (S T : Subalgebra R A) : (S ⊔ T).toSubsemiring = S.toSubsemiring ⊔ T.toSubsemiring :=
by
rw [← S.toSubsemiring.closure_eq, ← T.toSubsemiring.closure_eq, ← Subsemiring.closure_union]
simp_rw [sup_def, adjoin_toSubsemiring, Subalgebra.coe_toSubsemiring]
congr 1
rw [Set.union_eq_right]
rintro _ ⟨x, rfl⟩
exact Set.mem_union_left _ (algebraMap_mem S x)
