English
The think operation preserves membership: for any s and a, a belongs to think(s) if and only if a belongs to s.
Русский
Операция think сохраняет принадлежность: для любой последовательности s и элемента a выполняется a ∈ think(s) тогда и только тогда, когда a ∈ s.
LaTeX
$$$$\forall s:\\mathrm{WSeq}\,\alpha,\forall a:\\alpha,\ a \in \mathrm{think}\,s \iff a \in s.$$$$
Lean4
@[simp]
theorem mem_think (s : WSeq α) (a) : a ∈ think s ↔ a ∈ s :=
by
obtain ⟨f, al⟩ := s
change (some (some a) ∈ some none :: f) ↔ some (some a) ∈ f
constructor <;> intro h
· apply (Stream'.eq_or_mem_of_mem_cons h).resolve_left
intro
injections
· apply Stream'.mem_cons_of_mem _ h
