Theorems · Theorem · nonassociative algebras

NonUnitalSubalgebra.coe_iSup_of_directed

∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι]
  {S : ι → NonUnitalSubalgebra R A}, Directed (fun x1 x2 => x1 ≤ x2) S → ↑(iSup S) = ⋃ i, ↑(S i)

Defined in

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Cited by

2 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringNonUnitalNonAssocSemiringModuleIsScalarTowerSMulCommClassNonempty