subset_of_forall_subset — Mathlib

English

Let B be a topological basis. If s is open and every basis member U ⊆ s implies U ⊆ t, then s ⊆ t.

Русский

Пусть B — топологическая база. Если s открыто и каждый элемент базы U ⊆ s влечет U ⊆ t, то s ⊆ t.

LaTeX

$$subset_of_forall_subset {t : Set α} (hB : IsTopologicalBasis B) (hs : IsOpen s) (h : ∀ U ∈ B, U ⊆ s → U ⊆ t) : s ⊆ t$$

Lean4

theorem subset_of_forall_subset {t : Set α} (hB : IsTopologicalBasis B) (hs : IsOpen s) (h : ∀ U ∈ B, U ⊆ s → U ⊆ t) :
    s ⊆ t := by rw [hB.open_eq_sUnion' hs]; simpa [sUnion_subset_iff]

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