antisymm — Mathlib

English

If there are embeddings α ↪ β and β ↪ α, there exists an equivalence α ≃ β.

Русский

Если существуют вложения α ↪ β и β ↪ α, то существует эквивалентность α ≃ β.

LaTeX

$$For embeddings a: α ↪ β and b: β ↪ α, there exists Nonempty (α ≃ β).$$

Lean4

/-- **The Schröder-Bernstein Theorem**: Given embeddings `α ↪ β` and `β ↪ α`, there exists an
equivalence `α ≃ β`. -/
theorem antisymm : (α ↪ β) → (β ↪ α) → Nonempty (α ≃ β)
  | ⟨_, h₁⟩, ⟨_, h₂⟩ =>
    let ⟨f, hf⟩ := schroeder_bernstein h₁ h₂
    ⟨Equiv.ofBijective f hf⟩

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