separatesPoints_monotone — Mathlib

English

The map s ↦ s.SeparatesPoints is monotone: if s ⊆ t and s separates points, then t also separates points.

Русский

Отображение s ↦ s.SeparatesPoints монотонно: если s ⊆ t и s разделяет точки, то и t разделяет точки.

LaTeX

$$$\\text{Monotone }(s \\mapsto s.SeparatesPoints) : \\text{If } s \\subseteq t \\text{ and } s.SeparatesPoints \\text{ then } t.SeparatesPoints.$$$

Lean4

theorem separatesPoints_monotone : Monotone fun s : Subalgebra R C(α, A) => s.SeparatesPoints := fun s s' r h x y n =>
  by
  obtain ⟨f, m, w⟩ := h n
  rcases m with ⟨f, ⟨m, rfl⟩⟩
  exact ⟨_, ⟨f, ⟨r m, rfl⟩⟩, w⟩

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