groupFilterBasisOfComm — Mathlib

Lean4
/-- `GroupFilterBasis` constructor in the commutative group case. -/
@[to_additive /-- `AddGroupFilterBasis` constructor in the additive commutative group case. -/
    ]
def groupFilterBasisOfComm {G : Type*} [CommGroup G] (sets : Set (Set G)) (nonempty : sets.Nonempty)
    (inter_sets : ∀ x y, x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y) (one : ∀ U ∈ sets, (1 : G) ∈ U)
    (mul : ∀ U ∈ sets, ∃ V ∈ sets, V * V ⊆ U) (inv : ∀ U ∈ sets, ∃ V ∈ sets, V ⊆ (fun x ↦ x⁻¹) ⁻¹' U) :
    GroupFilterBasis G :=
  { sets := sets
    nonempty := nonempty
    inter_sets := inter_sets _ _
    one' := one _
    mul' := mul _
    inv' := inv _
    conj' := fun x U U_in ↦ ⟨U, U_in, by simp only [mul_inv_cancel_comm, preimage_id']; rfl⟩ }
Похожие утверждения