fst_surjective

Mathlib.Data.Sigma.Basic

URI: https://scilib.ai/kg/mathlib#Sigma.fst_surjective

Lean4

theorem fst_surjective [h : ∀ a, Nonempty (β a)] : Surjective (fst : (Σ a, β a) → α) := fun a ↦
  let ⟨b⟩ := h a;
  ⟨⟨a, b⟩, rfl⟩

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

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

Разделы

Аффилиация

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