inter_preimage_setOf_minimal_eq_of_subset

English

If t is contained in f''s, then the membership of x in s ∩ f^{-1}t is equivalent to membership of f x in t with respect to minimality.

Русский

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

LaTeX

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

Lean4

theorem inter_preimage_setOf_minimal_eq_of_subset (hts : t ⊆ f '' s) :
    x ∈ s ∩ f ⁻¹' {y | Minimal (· ∈ t) y} ↔ Minimal (· ∈ s ∩ f ⁻¹' t) x := by
  simp_rw [mem_inter_iff, preimage_setOf_eq, mem_setOf_eq, mem_preimage,
    f.minimal_apply_mem_iff (hts.trans (image_subset_range _ _)),
    minimal_and_iff_left_of_imp (fun _ hx ↦ f.injective.mem_set_image.1 <| hts hx)]

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