specializes_iff — Mathlib

English

If f is an inducing map, then f preserves specialization: f(x) ⤳ f(y) iff x ⤳ y.

Русский

Если отображение является индуцирующим, то оно сохраняет специализацию: f(x) ⤳ f(y) эквивалентно x ⤳ y.

LaTeX

$$$$\forall X\ Y, [\text{TopologicalSpace } X], [\text{TopologicalSpace } Y],\ {x,y:X}, {f:X\to Y},\ IsInducing f \Rightarrow (f\,x \rightsquigarrow f\,y \iff x \rightsquigarrow y).$$$$

Lean4

theorem specializes_iff (hf : IsInducing f) : f x ⤳ f y ↔ x ⤳ y := by
  simp only [specializes_iff_mem_closure, hf.closure_eq_preimage_closure_image, image_singleton, mem_preimage]

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