mem_closure_iff_exists_term — Mathlib

English

The membership of x in the closure of s is equivalent to the existence of a term t with variables from s such that t.realize((↑): s → M) = x.

Русский

Принадлежность x замыканию от s эквивалентна существованию терма t с переменными из s, для которого t.realize((↑): s → M) = x.

LaTeX

$$$$ x \in \operatorname{closure}_L(s) \iff \exists t : L\mathrm{Term}(s), \ t.realize((\uparrow) : s \to M) = x. $$$$

Lean4

theorem mem_closure_iff_exists_term {x : M} : x ∈ closure L s ↔ ∃ t : L.Term s, t.realize ((↑) : s → M) = x := by
  rw [← SetLike.mem_coe, coe_closure_eq_range_term_realize, mem_range]

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