embeddingOfSubset — Mathlib

English

There is an embedding from a subset s to t whenever s ⊆ t, given by inclusion.

Русский

Существует вложение из подмножества s в t при условии s ⊆ t, заданное включением.

LaTeX

$$$\\text{embeddingOfSubset } s\\; t\\; h : s \\hookrightarrow t$$$

Lean4

/-- The injection map is an embedding between subsets. -/
@[simps apply_coe]
def embeddingOfSubset {α} (s t : Set α) (h : s ⊆ t) : s ↪ t :=
  ⟨fun x ↦ ⟨x.1, h x.2⟩, fun ⟨x, hx⟩ ⟨y, hy⟩ h ↦ by
    congr
    injection h⟩

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