closure_eq_of_le — Mathlib

English

Let G be a group, K a subgroup of G, and k a subset of G. If k is contained in K and K is contained in the closure of k, then the closure of k equals K.

Русский

Пусть G — группа, K — подгруппа G, и k — подмножество G. Если k ⊆ K и K ⊆ замыкание(k), то замыкание(k) = K.

LaTeX

$$$ (k \subseteq K) \land (K \le \mathrm{closure}(k)) \Rightarrow \mathrm{closure}(k) = K $$$

Lean4

@[to_additive]
theorem closure_eq_of_le (h₁ : k ⊆ K) (h₂ : K ≤ closure k) : closure k = K :=
  le_antisymm ((closure_le <| K).2 h₁) h₂

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