distinctConstantsTheory_mono — Mathlib

English

DistinctConstantsTheory(s) is equivalent to the set of sentences stating pairwise distinctness of constants indexed by s.

Русский

Теория различимости констант для s эквивалентна множеству предложений о попарной различности констант, индексируемых элементами s.

LaTeX

$$$L.\\mathrm{distinctConstantsTheory}(s) = \\{ c_a \\neq c_b \\\\mid a,b \\in s, a \\neq b \\}$$$

Lean4

theorem distinctConstantsTheory_mono {s t : Set α} (h : s ⊆ t) :
    L.distinctConstantsTheory s ⊆ L.distinctConstantsTheory t := by unfold distinctConstantsTheory; gcongr

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