inv — Mathlib

English

For every U ∈ B there exists V ∈ B with V ⊆ (fun x ↦ x⁻¹)⁻¹' U; i.e., V is contained in the preimage of U under inversion.

Русский

Для каждого U ∈ B существует V ∈ B, такой что V ⊆ inv⁻¹'(U).

LaTeX

$$U \in B \Rightarrow \exists V \in B, V \subseteq (fun x \mapsto x^{-1})^{-1}' U$$

Lean4

@[to_additive]
theorem inv {U : Set G} : U ∈ B → ∃ V ∈ B, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U :=
  GroupFilterBasis.inv'

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