preimage — Mathlib

English

If s and t form a complement pair, then their preimages under f form a complement pair as well.

Русский

Если s и t образуют пару дополнений, то их прообраза по f образуют пару дополнений.

LaTeX

$$$\operatorname{IsCompl}(f^{-1}(s), f^{-1}(t))$ given $\operatorname{IsCompl}(s,t)$$$

Lean4

theorem preimage (f : α → β) {s t : Set β} (h : IsCompl s t) : IsCompl (f ⁻¹' s) (f ⁻¹' t) :=
  ⟨h.1.preimage f, h.2.preimage f⟩

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