coe_pi — Mathlib

English

Equality of underlying sets: (pi I H) as a set equals Set.pi I (H i as sets).

Русский

Равенство подлежащих множеств: (pi I H) как множество равно Set.pi I (H i как множества).

LaTeX

$$$ (\mathrm{pi} I H : \mathrm{Set}(\Pi i, f i)) = \mathrm{Set.pi} I (\lambda i, (H i : \mathrm{Set}(f i))) $$$

Lean4

@[to_additive]
theorem coe_pi (I : Set η) (H : ∀ i, Subgroup (f i)) :
    (pi I H : Set (∀ i, f i)) = Set.pi I fun i => (H i : Set (f i)) :=
  rfl

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