maximal_mem_image_iff — Mathlib

English

In an OrderEmbedding setting, maximal elements map to maximal elements via the embedding.

Русский

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

LaTeX

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

Lean4

theorem maximal_mem_image_iff (ha : a ∈ s) : Maximal (· ∈ f '' s) (f a) ↔ Maximal (· ∈ s) a :=
  _root_.maximal_mem_image_monotone_iff ha (by simp [f.le_iff_le])

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