seqLeft_def

Mathlib.Data.Set.Functor

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

English

The left-sequential product s <* t equals {a ∈ α | a ∈ s and t is nonempty}.

Русский

Левый секвенс-произведение s <* t равно {a ∈ α | a ∈ s и t непусто}.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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