leftRel_pi — Mathlib

English

LeftRel on the Pi-subgroup over Set.univ is the Pi of LeftRel on each component.

Русский

LeftRel на Pi-подгруппе над Set.univ есть Pi-отношение LeftRel по каждой компоненте.

LaTeX

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

Lean4

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

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