exists_structureMap_eq_of_forall — Mathlib

English

If x ∈ ∏ i A_i, then there exists x' ∈ ∏ i A_i such that structureMap R A 𝓕 x' = x.

Русский

Если x ∈ ∏ i A_i, то существует x' ∈ ∏ i A_i такое, что structureMap R A 𝓕 x' = x.

LaTeX

$$$\\forall x : \\prod_i A_i,\\; \\exists x' : \\prod_i A_i,\\; \\mathrm{structureMap}(R,A,𝓕)(x') = x.$$$

Lean4

theorem exists_structureMap_eq_of_forall {x : Πʳ i, [R i, A i]_[𝓕]} (hx : ∀ i, x.1 i ∈ A i) :
    ∃ x' : Π i, A i, structureMap R A 𝓕 x' = x :=
  ⟨fun i ↦ ⟨x i, hx i⟩, rfl⟩

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