inclusion_inj

Mathlib.Data.Set.Inclusion

URI: https://scilib.ai/kg/mathlib#Set.inclusion_inj

English

For h: s ⊆ t, x,y ∈ s, inclusion(h)(x) = inclusion(h)(y) iff x = y.

Русский

Для h: s ⊆ t, x,y ∈ s, inclusion(h)(x) = inclusion(h)(y) эквивалентно x = y.

LaTeX

$$$\forall x,y:\, s,\ inclusion(h)(x) = inclusion(h)(y) \iff x = y.$$$

Lean4

theorem inclusion_inj (h : s ⊆ t) {x y : s} : inclusion h x = inclusion h y ↔ x = y :=
  (inclusion_injective h).eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru