seqRight_def — Mathlib

English

The right sequencing s *> t equals ∅ if s is empty, otherwise it equals t.

Русский

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

LaTeX

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

Lean4

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

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