setOf_index_eq_univ — Mathlib

English

The set of all labelled roots equals the universal set; the indexed image over roots covers all possible roots up to sign and negation included in the indexing.

Русский

Множество помеченных корней совпадает с общим множеством; образ индекса по корням охватывает все корни (включая знаки и отрицания).

LaTeX

$$Set.univ = Set.instInsert.insert longRoot P ...$$

Lean4

theorem setOf_index_eq_univ :
    letI _i := P.indexNeg
    {long P, -long P, short P, -short P, shortAddLong P, -shortAddLong P, twoShortAddLong P, -twoShortAddLong P,
        threeShortAddLong P, -threeShortAddLong P, threeShortAddTwoLong P, -threeShortAddTwoLong P} =
      univ :=
  eq_univ_iff_forall.mpr fun i ↦ by simpa using mem_allRoots P i

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