field_closure_preimage_le — Mathlib

English

For f: K →+* L and s ⊆ L, closure(f^{-1}(s)) ≤ (closure s).comap f.

Русский

Для f: K →+* L и подмножества s ⊆ L выполнено closure(f^{-1}(s)) ≤ (closure s).comap f.

LaTeX

$$$\operatorname{closure}(f^{-1}[s]) \le (\operatorname{closure} s).comap f$$$

Lean4

theorem field_closure_preimage_le (f : K →+* L) (s : Set L) : closure (f ⁻¹' s) ≤ (closure s).comap f :=
  closure_le.2 fun _ hx => SetLike.mem_coe.2 <| mem_comap.2 <| subset_closure hx

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