rightRel_pi — Mathlib

English

RightRel on the Pi-subgroup equals the Pi-setoid of RightRel on components.

Русский

RightRel на Pi-подгруппе равен Pi-oid RightRel на компонентах.

LaTeX

$$$\text{RightRel}(\mathrm{Subgroup}.pi\;\mathrm{Set.univ}\; s') = @\text{piSetoid} _ _ (\lambda i \mapsto \text{RightRel}(s'(i)))$$$

Lean4

@[to_additive]
theorem rightRel_pi {ι : Type*} {β : ι → Type*} [∀ i, Group (β i)] (s' : ∀ i, Subgroup (β i)) :
    rightRel (Subgroup.pi Set.univ s') = @piSetoid _ _ fun i ↦ rightRel (s' i) :=
  by
  refine Setoid.ext fun x y ↦ ?_
  simp [Setoid.piSetoid_apply, rightRel_apply, Subgroup.mem_pi]

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