inter_preimage_setOf_maximal_eq_of_subset

English

If t ⊆ f''s, then the membership of x in s ∩ f^{-1}t corresponds to maximality in the preimage domain.

Русский

Если t ⊆ f''s, то членство x в s ∩ f^{-1}t соответствует максимальности в области предобраза.

LaTeX

$$$\\forall (hts : t \\subseteq f'' s),\\; x \\in s \\cap f^{-1}'{y\\mid \\operatorname{Maximal}(\\cdot \\in t) y} \\Leftrightarrow \\operatorname{Maximal}(\\cdot \\in s \\cap f^{-1}'t) x$$$

Lean4

theorem inter_preimage_setOf_maximal_eq_of_subset (hts : t ⊆ f '' s) :
    x ∈ s ∩ f ⁻¹' {y | Maximal (· ∈ t) y} ↔ Maximal (· ∈ s ∩ f ⁻¹' t) x :=
  f.dual.inter_preimage_setOf_minimal_eq_of_subset hts

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