core_union_subset — Mathlib

English

The union of cores is contained in the core of the union: R.core(t1) ∪ R.core(t2) ⊆ R.core(t1 ∪ t2).

Русский

Объединение ядер подмножеств содержится в ядре объединения: R.core(t1) ∪ R.core(t2) ⊆ R.core(t1 ∪ t2).

LaTeX

$$R.\mathrm{core}(t_1) \cup R.\mathrm{core}(t_2) \subseteq R.\mathrm{core}(t_1 \cup t_2)$$

Lean4

theorem core_union_subset : R.core t₁ ∪ R.core t₂ ⊆ R.core (t₁ ∪ t₂) :=
  core_mono.le_map_sup ..

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