range_inter_ssubset_iff_preimage_ssubset

English

For f: α → β and s,s' ⊆ β, range f ∩ s ⊂ range f ∩ s' iff f^{-1}(s) ⊂ f^{-1}(s').

Русский

Для отображения f: α → β и подмножеств s, s' ⊆ β: range f ∩ s ⊂ range f ∩ s' эквивалентно f^{-1}(s) ⊂ f^{-1}(s').

LaTeX

$$$ \\text{range } f \\cap s \\;\\subset\\; \\text{range } f \\cap s' \\;\\iff\\; f^{-1}(s) \\;\\subset\\; f^{-1}(s'). $$$

Lean4

theorem range_inter_ssubset_iff_preimage_ssubset {f : α → β} {s s' : Set β} :
    range f ∩ s ⊂ range f ∩ s' ↔ f ⁻¹' s ⊂ f ⁻¹' s' :=
  by
  simp only [Set.ssubset_iff_exists]
  apply and_congr ?_ (by aesop)
  constructor
  all_goals
    intro r x hx
    simp_all only [subset_inter_iff, inter_subset_left, true_and, mem_preimage, mem_inter_iff, mem_range, true_and]
    aesop

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