instCanLiftSetCoeAndMemOfNatForallForallForallForallHMulForallForallInv

English

There exists a CanLift structure from Set G to Subgroup G with carrier s satisfying 1 ∈ s, closure under multiplication, and closure under inversion.

Русский

Существует структура CanLift от Set G к Subgroup G, если носитель s удовлетворяет 1 ∈ s, замкнутости при умножении и обратимости.

LaTeX

$$$$ \\text{CanLift}(\\mathrm{Set} G, \\mathrm{Subgroup} G, \\iota, \\text{predicate}) $$ where predicate := 1 \\in s ∧ (∀ x,y ∈ s, xy ∈ s) ∧ (∀ x ∈ s, x^{-1} ∈ s). $$$$

Lean4

@[to_additive]
instance (priority := 100) :
    CanLift (Set G) (Subgroup G) (↑) (fun s ↦ 1 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x}, x ∈ s → x⁻¹ ∈ s)
    where
  prf s
    h :=
    ⟨{ carrier := s, one_mem' := h.1, mul_mem' := h.2.1, inv_mem' := h.2.2 }, rfl⟩
      -- TODO: Below can probably be written more uniformly

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