mem_iff_eq_image

Mathlib.Logic.Function.FiberPartition

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

← MathLib Explorer

English

For y and a fiber a of f, y ∈ a.val iff f y = a.image.

Русский

Для y и волокна a функции f, y принадлежит a.val тогда и только тогда, когда f y = a.image.

LaTeX

$$$y \in a.\mathrm{val} \iff f\,y = a.image$$$

Lean4

theorem mem_iff_eq_image (f : Y → Z) (y : Y) (a : Fiber f) : y ∈ a.val ↔ f y = a.image :=
  ⟨fun h ↦ a.map_eq_image _ ⟨y, h⟩, fun h ↦ by rw [a.eq_fiber_image]; exact h⟩

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

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

Разделы

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

Аффилиация

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