seqRight_def

Mathlib.Data.Set.Functor

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

English

The right-sequential product s *> t equals {a | s is nonempty and a ∈ t}.

Русский

Правый последовательный продукт s *> t равен {a | s непусто и a ∈ t}.

LaTeX

$$$s *> t = \{a \mid s \neq \emptyset \land a \in t\}$$$

Lean4

@[simp]
theorem seqRight_def (s : Set α) (t : Set β) : s *> t = {a | s.Nonempty ∧ a ∈ t} :=
  rfl

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

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

Разделы

Аффилиация

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