mem_pullSub_self — Mathlib

English

Let A be a type and T a tree on A, and x a list of A. Then x is an element of pullSub T x if and only if the empty list is an element of T.

Русский

Пусть A — тип, T — дерево над A, и x — список над A. Тогда x ∈ pullSub T x тогда и только тогда, когда [] ∈ T.

LaTeX

$$$ x \in \operatorname{pullSub} T x \;\Leftrightarrow\; [] \in T $$$

Lean4

@[simp]
theorem mem_pullSub_self : x ∈ pullSub T x ↔ [] ∈ T := by simpa using mem_pullSub_append (y := [])

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