mem_map_iff_exists_image — Mathlib

English

For any t, t ∈ map m f if and only if there exists s ∈ f such that m''s ⊆ t.

Русский

Для любого t выполняется: t входит в map m f тогда и только если существует s ∈ f такое, что m''s ⊆ t.

LaTeX

$$t ∈ map m f ↔ ∃ s ∈ f, m '' s ⊆ t$$

Lean4

theorem mem_map_iff_exists_image : t ∈ map m f ↔ ∃ s ∈ f, m '' s ⊆ t :=
  ⟨fun ht => ⟨m ⁻¹' t, ht, image_preimage_subset _ _⟩, fun ⟨_, hs, ht⟩ => mem_of_superset (image_mem_map hs) ht⟩

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