maximal_apply_mem_inter_range_iff

English

Dual statements: maximal in t ∩ range f correspond to maximal in t via duality.

Русский

Двойственные утверждения: максимальные в t ∩ range f соответствуют максимальным через двойственность.

LaTeX

$$$\\forall f:\\, \\text{OrderEmbedding }\\alpha\\to\\beta,\\; \\text{Maximal}(\\cdot \\in t \\cap \\operatorname{range}f) (f x) \\iff \\text{Maximal}(\\cdot \\in t) (f x)$$$

Lean4

theorem maximal_apply_mem_inter_range_iff : Maximal (· ∈ t ∩ range f) (f x) ↔ Maximal (fun x ↦ f x ∈ t) x :=
  f.dual.minimal_apply_mem_inter_range_iff

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