instInvCoeOfInvMemClass — Mathlib

English

If h is a relation 𝓕 ≤ 𝓖 and x is in the 𝓕-restricted product with hx, there exists x' in the 𝓖-restricted product such that inclusion h x' = x.

Русский

Если 𝓕 ≤ 𝓖 и x принадлежит ограниченному произведению по 𝓕, то существует x' в ограниченном произведении по 𝓖, удовлетворяющее inclusion h x' = x.

LaTeX

$$$\\exists x' : \\mathrm{RestrictedProduct}_{𝓖},\\; \\mathrm{inclusion}(h)(x') = x.$$$

Lean4

@[to_additive]
instance [Π i, Inv (R i)] [∀ i, InvMemClass (S i) (R i)] : Inv (Πʳ i, [R i, B i]_[𝓕]) where
  inv x := ⟨fun i ↦ (x i)⁻¹, x.2.mono fun _ ↦ inv_mem⟩

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