enlarge — Mathlib

English

If S is coherent with S and every s∈S is contained in some t∈T, then T is coherent.

Русский

Если S когерентно, и каждый s∈S содержится в некотором t∈T, то T когерентно.

LaTeX

$$$ \\text{IsCoherentWith } S \\to (\\forall s \\in S, \\exists t \\in T, s \\subseteq t) \\to \\text{IsCoherentWith } T $$$

Lean4

protected theorem enlarge {T} (hS : IsCoherentWith S) (hT : ∀ s ∈ S, ∃ t ∈ T, s ⊆ t) : IsCoherentWith T :=
  of_continuous_prop fun _f hf ↦
    hS.continuous_iff.2 fun s hs ↦
      let ⟨t, htT, hst⟩ := hT s hs;
      (hf t htT).mono hst

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