exists_of_mem_map

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.Chain.exists_of_mem_map

English

If b ∈ c.map f, there exists a with a ∈ c and f(a) = b.

Русский

Если b ∈ c.map f, существует a, такой что a ∈ c и f(a) = b.

LaTeX

$$$\\exists a \\ (a \\in c \\land f(a) = b)$$$

Lean4

theorem exists_of_mem_map {b : β} : b ∈ c.map f → ∃ a, a ∈ c ∧ f a = b := fun ⟨i, h⟩ => ⟨c i, ⟨i, rfl⟩, h.symm⟩

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

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

Разделы

Аффилиация

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