isMin_apply_iff — Mathlib

English

Minima are preserved by the embedding: IsMin(f(a)) if and only if IsMin(a).

Русский

Минимальность сохраняется сквозь встраивание: IsMin(f(a)) тогда и только тогда, когда IsMin(a).

LaTeX

$$IsMin(f(a)) \iff IsMin(a)$$

Lean4

@[simp]
theorem isMin_apply_iff [PartialOrder α] (f : α ≤i β) : IsMin (f a) ↔ IsMin a :=
  by
  refine ⟨StrictMono.isMin_of_apply f.strictMono, fun h b hb ↦ ?_⟩
  obtain ⟨x, rfl⟩ := f.mem_range_of_le hb
  rw [f.le_iff_le] at hb ⊢
  exact h hb

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