supports_singleton — Mathlib

English

A singleton set {q} is S-supported exactly when the trace of q is TM2-supported with respect to S.

Русский

Множество вида {q} поддерживается по S тогда и только тогда, когда трейс q поддерживается TM2 относительно S.

LaTeX

$$$\\mathrm{Supports}(\\{q\\}, S) \\iff \\mathrm{TM2.SupportsStmt}(S, \\mathrm{tr}(q)).$$$

Lean4

theorem supports_singleton {S q} : Supports { q } S ↔ TM2.SupportsStmt S (tr q) := by simp [Supports]

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