coe_inclusionEmbedding — Mathlib

English

Let r be a relation on α and S ⊆ T be subsets. The natural inclusion embedding from S to T coincides with the set-theoretic inclusion map.

Русский

Пусть r — отношение на α и S ⊆ T — подмножества. Естественное вложение из S в T совпадает с обычным включением множеств.

LaTeX

$$$ (Subrel.inclusionEmbedding\; r\; h) =\\; Set.inclusion\\; h, $$$

Lean4

@[simp]
theorem coe_inclusionEmbedding (r : α → α → Prop) {s t : Set α} (h : s ⊆ t) :
    (Subrel.inclusionEmbedding r h : s → t) = Set.inclusion h :=
  rfl

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