conj — Mathlib

English

For any x0 ∈ G and U ∈ B there exists V ∈ B with V ⊆ (x0 x x0⁻¹)⁻¹' U; i.e., V is contained in the preimage of U under conjugation by x0.

Русский

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

LaTeX

$$∃ V ∈ B, V ⊆ (fun x ↦ x0 * x * x0^{-1})^{-1}' U$$

Lean4

@[to_additive]
theorem conj : ∀ x₀, ∀ {U}, U ∈ B → ∃ V ∈ B, V ⊆ (fun x ↦ x₀ * x * x₀⁻¹) ⁻¹' U :=
  GroupFilterBasis.conj'

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