preimage_subset_core — Mathlib

English

The preimage of s under f is contained in the core of s with respect to f: f.preimage s ⊆ f.core s.

Русский

Предобраз множества s по f содержится в ядре s по отношению к f: f.preimage s ⊆ f.core s.

LaTeX

$$$$ f.preimage(s) \subseteq f.core(s). $$$$

Lean4

theorem preimage_subset_core (f : α →. β) (s : Set β) : f.preimage s ⊆ f.core s := fun _ ⟨y, ys, fxy⟩ y' fxy' =>
  have : y = y' := Part.mem_unique fxy fxy'
  this ▸ ys

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