isMax_apply — Mathlib

English

An order isomorphism preserves maximal elements: IsMax(x) holds iff IsMax(f(x)).

Русский

Изоморфизм порядка сохраняет максимальные элементы: IsMax(x) эквивалично IsMax(f(x)).

LaTeX

$$$ IsMax(f(x)) \iff IsMax(x) $$$

Lean4

theorem isMax_apply {α β : Type*} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} : IsMax (f x) ↔ IsMax x :=
  by
  refine ⟨f.strictMono.isMax_of_apply, ?_⟩
  conv_lhs => rw [← f.symm_apply_apply x]
  exact f.symm.strictMono.isMax_of_apply

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