mono — Mathlib

English

If t ≤ u are topologies on S and a has an evaluation with respect to t, then a has an evaluation with respect to u.

Русский

Если топология t на S слишком же слабая по отношению к u (t ≤ u) и для a существует оценка при t, то существует оценка и при u.

LaTeX

$$$t \le u \rightarrow HasEval a \,\text{(under } t) \rightarrow HasEval a \,\text{(under } u)$$$

Lean4

theorem mono {S : Type*} [CommRing S] {a : S} {t u : TopologicalSpace S} (h : t ≤ u) (ha : @HasEval _ _ t a) :
    @HasEval _ _ u a := by
  simp only [hasEval_iff] at ha ⊢
  exact ha.mono h

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