mk_subset_ge_of_subset_image — Mathlib

English

If t ⊆ f''s, then |t| ≤ |{x ∈ s | f x ∈ t}| after lifting.

Русский

Если t ⊆ образ f(s), то |t| ≤ |{x ∈ s | f x ∈ t}| после подъёма.

LaTeX

$$$|t| \\le |\\{x \\in s \\mid f x \\in t\\}|$$$

Lean4

theorem mk_subset_ge_of_subset_image (f : α → β) {s : Set α} {t : Set β} (h : t ⊆ f '' s) :
    #t ≤ #({x ∈ s | f x ∈ t} : Set α) := by
  rw [image_eq_range] at h
  convert mk_preimage_of_subset_range _ _ h using 1
  rw [mk_sep]
  rfl

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