Iio_injective

Mathlib.Order.Interval.Set.LinearOrder

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

English

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

Русский

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

LaTeX

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

Lean4

theorem Iio_injective : Injective (Iio : α → Set α) := fun _ _ => eq_of_forall_lt_iff ∘ Set.ext_iff.1

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

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

Разделы

Аффилиация

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