singleton_sups

Mathlib.Data.Set.Sups

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

English

The sups operation with a singleton on the left distributes over a set t: {a} ⊻ t = t.image (λ b, a ⊔ b).

Русский

Один элемент слева распространяется над множеством: {a} ⊻ t = t.image(λ b, a ⊔ b).

LaTeX

$$$ {a} \\veebar t = t.image (\\lambda b \\; a \\veebar b) $$$

Lean4

@[simp]
theorem singleton_sups : { a } ⊻ t = t.image fun b => a ⊔ b :=
  image2_singleton_left

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

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

Разделы

Аффилиация

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