isMin_apply — Mathlib

English

An order isomorphism preserves minimal elements: IsMin(x) holds iff IsMin(f(x)).

Русский

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

LaTeX

$$$ IsMin(f(x)) \iff IsMin(x) $$$

Lean4

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

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