preimage — Mathlib

English

If s and t are disjoint in β, then their preimages under f are disjoint in α.

Русский

Если s и t на β непересекаются, то их прообраза по f на α непересекаются.

LaTeX

$$$\operatorname{Disjoint}(f^{-1}(s), f^{-1}(t)) \text{ if } \operatorname{Disjoint}(s,t)$$$

Lean4

theorem preimage (f : α → β) {s t : Set β} (h : Disjoint s t) : Disjoint (f ⁻¹' s) (f ⁻¹' t) :=
  disjoint_iff_inf_le.mpr fun _ hx => h.le_bot hx

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