sup — Mathlib

English

The supremum of two countably generated measurable spaces is countably generated.

Русский

Объединение двух счётно порождаемых измеримых пространств остаётся счётно порождаемым.

LaTeX

$$$ \forall m_1 m_2, CountablyGenerated m_1 \to CountablyGenerated m_2 \to CountablyGenerated (m_1 \sqcup m_2) $$$

Lean4

theorem sup {m₁ m₂ : MeasurableSpace β} (h₁ : @CountablyGenerated β m₁) (h₂ : @CountablyGenerated β m₂) :
    @CountablyGenerated β (m₁ ⊔ m₂) := by
  rcases h₁ with ⟨⟨b₁, hb₁c, rfl⟩⟩
  rcases h₂ with ⟨⟨b₂, hb₂c, rfl⟩⟩
  exact @mk _ (_ ⊔ _) ⟨_, hb₁c.union hb₂c, generateFrom_sup_generateFrom⟩

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