exists_i₂ — Mathlib

English

If e1 and e2 form a complementary pair of embeddings, then for every i in the target index set ι, whenever i is not in the image of e1, there exists i2 in ι2 with i = e2.f(i2).

Русский

Если e1 и e2 образуют комплементарную пару вложений между геометриями, то для каждого i из целевого множества индексов итерировании, если i не лежит в образе e1, существует i2 из ι2 такое, что i = e2.f(i2).

LaTeX

$$$\forall i \in \iota,\ (\forall i_1 \in \iota_1,\ e_1.f(i_1) \neq i) \Rightarrow \exists i_2 \in \iota_2\ i = e_2.f(i_2).$$$

Lean4

theorem exists_i₂ (i : ι) (hi : ∀ i₁, e₁.f i₁ ≠ i) : ∃ i₂, i = e₂.f i₂ :=
  ac.symm.exists_i₁ i hi

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