image_setOf_maximal — Mathlib

English

For an order-embedding f, the image of maximal elements equals the set of maximal elements in the image set.

Русский

Для вложения порядка f образ максимальных элементов равен множеству максимальных элементов образа.

LaTeX

$$$\\forall f:\\, \\text{OrderEmbedding }\\alpha \\to \\beta,\\; f''\\{x \\mid \\operatorname{Maximal}(\\cdot \\in s) x\\} = \\{x \\mid \\operatorname{Maximal}(\\cdot \\in f'' s) x\\}$$$

Lean4

@[simp]
theorem image_setOf_maximal : f '' {x | Maximal (· ∈ s) x} = {x | Maximal (· ∈ f '' s) x} :=
  _root_.image_monotone_setOf_maximal (by simp [f.le_iff_le])

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