maximal_apply_iff — Mathlib

English

If ht holds, a maximal in the image corresponds to a maximal in the domain.

Русский

Если ht выполнено, максимальное в образе соответствует максимальному в области.

LaTeX

$$$\\forall ht:\\; t \\subseteq \\operatorname{range}f,\\; \\big( \\text{Maximal}(\\cdot \\in t) (f x) \\iff \\text{Maximal}(\\cdot \\in t) x \\big)$$$

Lean4

theorem maximal_apply_iff (ht : t ⊆ Set.range f) : Maximal (· ∈ t) (f x) ↔ Maximal (fun x ↦ f x ∈ t) x :=
  f.dual.minimal_apply_mem_iff ht

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