core_mono — Mathlib

English

If s ⊆ t, then the core of s is contained in the core of t. In other words, enlarging the target set cannot shrink the core.

Русский

Если s ⊆ t, то ядро s ⊆ ядра t. Другими словами, расширение множества-множителя не уменьшает ядро.

LaTeX

$$$$ s \subseteq t \;\Rightarrow\; f.core(s) \subseteq f.core(t). $$$$

Lean4

theorem core_mono {s t : Set β} (h : s ⊆ t) : f.core s ⊆ f.core t :=
  SetRel.core_mono h

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