orElse_def

Mathlib.Data.Set.Functor

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

English

The orElse operation on sets is union: s <|> t = s ∪ t.

Русский

Операция orElse над множествами равна объединению: s <|> t = s ∪ t.

LaTeX

$$$s <|> t = s \cup t$$$

Lean4

@[simp]
theorem orElse_def (s : Set α) (t : Set α) : (s <|> t) = s ∪ t :=
  rfl

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

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

Разделы

Аффилиация

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