range_pair

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.Chain.range_pair

English

The range of the pair construction is exactly the set {a, b}.

Русский

Образ пары равен множеству {a, b}.

LaTeX

$$$$ \operatorname{Set.range}(\text{pair } a b hab) = \{a, b\}. $$$$

Lean4

@[simp]
theorem range_pair (a b : α) (hab) : Set.range (pair a b hab) = { a, b } := by ext;
  exact Nat.or_exists_add_one.symm.trans (by aesop)

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

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

Разделы

Аффилиация

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