inclusionEmbedding — Mathlib

English

The inclusion of a subset s into a larger set t extends to a RelEmbedding between the corresponding Subrel relations.

Русский

Включение подмножества s в большее множество t порождает отображение реляций между соответствующими Subrel.

LaTeX

$$RelEmbedding( Subrel r (x∈s) , Subrel r (x∈t) ) via Set.inclusion h$$

Lean4

/-- `Set.inclusion` as a relation embedding. -/
protected def inclusionEmbedding (r : α → α → Prop) {s t : Set α} (h : s ⊆ t) : Subrel r (· ∈ s) ↪r Subrel r (· ∈ t)
    where
  toFun := Set.inclusion h
  inj' _ _ h := (Set.inclusion_inj _).mp h
  map_rel_iff' := Iff.rfl

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