supports_insert — Mathlib

English

If you insert an element q into a set K, the resulting Supports (insert q K) S holds exactly when q is TM2-supported and the original K is S-supported.

Русский

Если добавить элемент q в множество K, полученное свойство Supports(insert q K, S) выполняется тогда и только тогда, когда q поддерживается TM2 и K поддерживается S.

LaTeX

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

Lean4

theorem supports_insert {K S q} : Supports (insert q K) S ↔ TM2.SupportsStmt S (tr q) ∧ Supports K S := by
  simp [Supports]

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