inv_apply — Mathlib

English

The range of the structure map consists of all pairs whose coordinate components lie in A_i for every i.

Русский

Образ structureMap состоит из пар, координаты которых попадают в A_i для каждого i.

LaTeX

$$$\\mathrm{range}(\\mathrm{structureMap}) = \\{ f : \\text{RestrictedProduct} \\mid \\forall i, f.1(i) \\in A_i \\}.$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_apply [Π i, Inv (R i)] [∀ i, InvMemClass (S i) (R i)] (x : Πʳ i, [R i, B i]_[𝓕]) (i : ι) :
    (x⁻¹) i = (x i)⁻¹ :=
  rfl

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