twoEmbeddingEquiv — Mathlib

English

There is a natural equivalence between embeddings Fin 2 → α and pairs of distinct elements of α; it sends an embedding to its two coordinate values and back.

Русский

Существует естественная эквивалентность между вложениями Fin 2 → α и парами различных элементов α; она отправляет вложение в его две координаты и обратно.

LaTeX

$$$\\text{twoEmbeddingEquiv} : (\\mathrm{Fin}\\ 2 \\hookrightarrow \\alpha) \\simeq \\{(a,b)\\in \\alpha\\times\\alpha \\mid a \\neq b\\}$$$

Lean4

/-- The natural equivalence of `Fin 2 ↪ α` with pairs `(a, b)` of distinct elements of `α`. -/
def twoEmbeddingEquiv : (Fin 2 ↪ α) ≃ {(a, b) : α × α | a ≠ b}
    where
  toFun
    e :=
    ⟨(e 0, e 1), by
      simp only [ne_eq, Fin.isValue, mem_setOf_eq, EmbeddingLike.apply_eq_iff_eq, zero_eq_one_iff, succ_ne_self,
        not_false_eq_true]⟩
  invFun := fun ⟨⟨a, b⟩, h⟩ ↦
    { toFun i := if i = 0 then a else b
      inj' i j
        hij := by
        by_cases hi : i = 0
        · by_cases hj : j = 0
          · simp [hi, hj]
          · simp only [if_pos hi, eq_one_of_ne_zero j hj, if_neg (Ne.symm Fin.zero_ne_one)] at hij
            apply (h hij).elim
        · rw [eq_one_of_ne_zero i hi] at hij ⊢
          by_cases hj : j = 0
          · simp [hj] at hij; exact False.elim (h hij.symm)
          · rw [eq_one_of_ne_zero j hj] }
  left_inv
    e := by
    ext i
    by_cases hi : i = 0
    · simp [hi]
    · simp [Fin.eq_one_of_ne_zero i hi]

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