mem_enum

Mathlib.Data.FinEnum

URI: https://scilib.ai/kg/mathlib#List.Pi.mem_enum

Lean4

theorem mem_enum (f : ∀ a, β a) : f ∈ Pi.enum β := by simpa [Pi.enum] using ⟨fun a _ => f a, mem_pi_toList _ _, rfl⟩

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

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

Разделы

Аффилиация

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