mono — Mathlib

English

If 𝒢 is IsSeparating and 𝒢 ⊆ ℋ, then ℋ is IsSeparating as well.

Русский

Если 𝒢 является разделяющим и 𝒢 ⊆ ℋ, то ℋ тоже является разделяющим.

LaTeX

$$$IsSeparating(\mathcal{G}) \wedge (\mathcal{G} \subseteq \mathcal{H}) \Rightarrow IsSeparating(\mathcal{H})$$$

Lean4

theorem mono {𝒢 : Set C} (h𝒢 : IsSeparating 𝒢) {ℋ : Set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) : IsSeparating ℋ := fun _ _ _ _ hfg =>
  h𝒢 _ _ fun _ hG _ => hfg _ (h𝒢ℋ hG) _

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