ofSet — Mathlib

English

If an S over R is generated by a set s, then the Generators R S s encode S via the adjoin of s equals top.

Русский

Если S над R порождается множеством s, то Generators R S s кодирует S через адjoin(s) = верх.

LaTeX

$$ofSet (hs) : Algebra.Generators R S s.Elem$$

Lean4

/-- Construct `Generators` from a family of generators of `S`. -/
noncomputable def ofSet {s : Set S} (hs : Algebra.adjoin R s = ⊤) : Generators R S s :=
  by
  refine ofSurjective (Subtype.val : s → S) ?_
  rwa [← AlgHom.range_eq_top, ← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe_subtype, Set.setOf_mem_eq]

Похожие утверждения