mono — Mathlib

English

Satisfiability is monotone with respect to inclusion of theories: if T' is satisfiable and T ⊆ T', then T is satisfiable.

Русский

Удовлетворимость монотонна по включению: если T' удовлетворима и T ⊆ T', то T удовлетворима.

LaTeX

$$$T' IsSatisfiable \\to T.IsSatisfiable \\text{ if } T \\subseteq T'$$$

Lean4

theorem mono (h : T'.IsSatisfiable) (hs : T ⊆ T') : T.IsSatisfiable :=
  ⟨(Theory.Model.mono (ModelType.is_model h.some) hs).bundled⟩

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