mem_onTheory — Mathlib

English

For any language map g, any theory T, and any sentence φ in the target language, φ belongs to g.onTheory(T) if and only if there exists φ0 ∈ T with g.onSentence(φ0) = φ.

Русский

Для отображения языка g, теории T и предложения φ из целевого языка, φ ∈ g.onTheory(T) тогда и только тогда, когда существует φ0 ∈ T такое, что g.onSentence(φ0) = φ.

LaTeX

$$$\\phi \\in g.onTheory(T) \\\\iff \\exists \\phi_0 \\in T,\\; g.onSentence(\\phi_0) = \\phi$$$

Lean4

@[simp]
theorem mem_onTheory {g : L →ᴸ L'} {T : L.Theory} {φ : L'.Sentence} :
    φ ∈ g.onTheory T ↔ ∃ φ₀, φ₀ ∈ T ∧ g.onSentence φ₀ = φ :=
  Set.mem_image _ _ _

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