Ioi_injective

Mathlib.Order.Interval.Set.LinearOrder

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

English

The map x ↦ Ioi x is injective: if Ioi x = Ioi y then x = y.

Русский

Отображение x ↦ Ioi x инъективно: если Ioi x = Ioi y, то x = y.

LaTeX

$$$\\text{Injective}(\\mathrm{Ioi}: \\alpha \\to \\mathcal{P}(\\alpha))$$$

Lean4

theorem Ioi_injective : Injective (Ioi : α → Set α) := fun _ _ => eq_of_forall_gt_iff ∘ Set.ext_iff.1

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

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

Разделы

Аффилиация

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