subset — Mathlib

English

If f is locally finite and each g_i is contained in f_i, then g is locally finite.

Русский

Если f локально конечна и каждый g_i ⊆ f_i, тогда {g_i} локально конечна.

LaTeX

$$LocallyFinite f → (∀ i, g i ⊆ f i) → LocallyFinite g$$

Lean4

protected theorem subset (hf : LocallyFinite f) (hg : ∀ i, g i ⊆ f i) : LocallyFinite g := fun a =>
  let ⟨t, ht₁, ht₂⟩ := hf a
  ⟨t, ht₁, ht₂.subset fun i hi => hi.mono <| inter_subset_inter (hg i) Subset.rfl⟩

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