exists_inclusion_eq_of_eventually

English

If h is a relation 𝓕 ≤ 𝓖 and x is a restricted product element with respect to 𝓕, and x_i ∈ A_i holds eventually in 𝓖, there exists x' in the 𝓖-restricted product with inclusion h x' = x.

Русский

Если h: 𝓕 ≤ 𝓖 и x ∈ RestrictedProduct(𝓕) установлен, а x_i ∈ A_i выполняетсяEventually в 𝓖, тогда существует x' в RestrictedProduct(𝓖) с включением h x' = x.

LaTeX

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

Lean4

theorem exists_inclusion_eq_of_eventually (h : 𝓕 ≤ 𝓖) {x : Πʳ i, [R i, A i]_[𝓕]} (hx𝓖 : ∀ᶠ i in 𝓖, x i ∈ A i) :
    ∃ x' : Πʳ i, [R i, A i]_[𝓖], inclusion R A h x' = x :=
  ⟨⟨x.1, hx𝓖⟩, rfl⟩

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