isChain_range

Mathlib.Order.OmegaCompletePartialOrder

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

English

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

Русский

Если b ∈ c.map f, существует a such that a ∈ c и f(a) = b.

LaTeX

$$b ∈ c.map f ⇒ ∃ a, a ∈ c ∧ f(a) = b$$

Lean4

theorem isChain_range : IsChain (· ≤ ·) (Set.range c) :=
  Monotone.isChain_range (OrderHomClass.mono c)

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

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

Разделы

Аффилиация

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