realize_toSentence_iff_toProp — Mathlib

English

A field axiom realizes to a sentence iff its corresponding property holds in the field.

Русский

Аксиома поля реализуется в предложение тогда и только тогда, когда соответствующее свойство выполняется в поле.

LaTeX

$$$(ax\text{.toSentence})$ realizable in K iff $ax$.toProp K$$

Lean4

theorem realize_toSentence_iff_toProp {K : Type*} [Add K] [Mul K] [Neg K] [Zero K] [One K] [CompatibleRing K]
    (ax : FieldAxiom) : (K ⊨ (ax.toSentence : Sentence Language.ring)) ↔ ax.toProp K := by
  cases ax <;> simp [Sentence.Realize, Formula.Realize, Fin.snoc]

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