range_some_inter_none

Mathlib.Data.Set.Image

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

English

The intersection of the range of some with { none } is empty.

Русский

Пересечение диапазона some с { none } пусто.

LaTeX

$$$$ \\operatorname{range}(\\text{some}) \\cap \\{ \\text{none} \\} = \\emptyset $$$$

Lean4

@[simp]
theorem range_some_inter_none (α : Type*) : range (some : α → Option α) ∩ { none } = ∅ :=
  (isCompl_range_some_none α).inf_eq_bot

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

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

Разделы

Аффилиация

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