fiber_nonempty

Mathlib.Logic.Function.FiberPartition

URI: https://scilib.ai/kg/mathlib#Function.Fiber.fiber_nonempty

← MathLib Explorer

English

The fiber a.val is nonempty; i.e., there exists an element in a.val.

Русский

Значение a.val непусто; существует элемент в a.val.

LaTeX

$$$\operatorname{Nonempty}(a.\mathrm{val})$$$

Lean4

theorem fiber_nonempty (f : Y → Z) (a : Fiber f) : Set.Nonempty a.val :=
  by
  refine ⟨preimage f a, ?_⟩
  rw [mem_iff_eq_image, ← map_preimage_eq_image]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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