seq_eq_set_seq

Mathlib.Data.Set.Functor

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

English

For any s ⊆ Set(α→β) and t ⊆ α, s <*> t equals s.seq t.

Русский

Для любых s ⊆ Set(α→β) и t ⊆ α верно s <*> t = s.seq t.

LaTeX

$$$s <*> t = s.seq t$$$

Lean4

@[simp]
theorem seq_eq_set_seq (s : Set (α → β)) (t : Set α) : s <*> t = s.seq t :=
  rfl

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

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

Разделы

Аффилиация

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