mem_map

Mathlib.Order.OmegaCompletePartialOrder

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

English

There is a membership relation that says a ∈ c if and only if a equals some value of c at some index.

Русский

Существует отношение принадлежности, что a ∈ c тогда, когда a равняется значению c на некотором индексе.

LaTeX

$$$ a \\in c \\iff \\exists i, a = c(i) $$$

Lean4

theorem mem_map (x : α) : x ∈ c → f x ∈ Chain.map c f := fun ⟨i, h⟩ => ⟨i, h.symm ▸ rfl⟩

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

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

Разделы

Аффилиация

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