seqLeft_def

Mathlib.Data.Finset.Functor

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

English

The left sequencing s <* t equals ∅ if t is empty, otherwise it equals s.

Русский

Левая последовательность s <* t равна пустому множеству, если t пусто, иначе равна s.

LaTeX

$$$$ s \\ltimes t = \\begin{cases} \\emptyset, & t = \\emptyset, \\\\ s, & \\text{otherwise}. \\end{cases} $$$$

Lean4

@[simp]
theorem seqLeft_def (s : Finset α) (t : Finset β) : s <* t = if t = ∅ then ∅ else s :=
  rfl

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

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

Разделы

Аффилиация

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