Subalgebra.coe_iSup_of_directed

theorem Subalgebra.coe_iSup_of_directed : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Type u_4} [inst_3 : Nonempty ι] {K : ι → Subalgebra R A}, Directed (fun x x_1 => x ≤ x_1) K → ↑(iSup K) = ⋃ i, ↑(K i)

This theorem states that for any commutative semiring `R`, semiring `A`, algebra structure of `A` over `R`, index type `ι` (which is nonempty), and a family `K` of subalgebras of `A` over `R`, if the family `K` is directed with respect to the inclusion relation (meaning that for any two subalgebras in the family, there is another subalgebra in the family that contains both), then the supremum of the family `K` (considered as elements of the complete lattice of subsets of `A`) is equal to the union of the sets of elements of the subalgebras in the family `K`. In other words, in this scenario, the supremum of a family of subalgebras is the subalgebra generated by the union of the subalgebras in the family.

More concisely: If `K` is a directed family of subalgebras of a commutative semiring `A` over semiring `R`, then the supremum of `K` equals the subalgebra generated by the union of the sets of elements of subalgebras in `K`.