hasEval — Mathlib

English

If a has substitution, then it also has evaluation: HasSubst a → HasEval a.

Русский

Если есть подстановка, то существует и оценивание: HasSubst a → HasEval a.

LaTeX

$$HasSubst a → HasEval a$$

Lean4

theorem hasEval [TopologicalSpace S] (ha : HasSubst a) : HasEval a :=
  HasEval.mono (instTopologicalSpace_mono τ bot_le) <|
    (@hasSubst_iff_hasEval_of_discreteTopology σ τ _ _ a ⊥ (@DiscreteTopology.mk S ⊥ rfl)).mp ha

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