instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMapForallForallStar

English

Equality of StarSubalgebras is determined by equality of their elements.

Русский

Равенство StarSubalgebra определяется по равенству элементов.

LaTeX

$$$\\forall S,T: StarSubalgebra\\ R\\ A,\\; S= T \\iff \\forall x, x\\in S \\leftrightarrow x\\in T$$$

Lean4

instance (priority := 100) :
    CanLift (Set A) (StarSubalgebra R A) (↑)
      (fun s ↦
        (∀ {x y}, x ∈ s → y ∈ s → x + y ∈ s) ∧
          (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ (∀ (r : R), algebraMap R A r ∈ s) ∧ ∀ {x}, x ∈ s → star x ∈ s)
    where
  prf s
    h :=
    ⟨{  carrier := s
        zero_mem' := by simpa using h.2.2.1 0
        add_mem' := h.1
        one_mem' := by simpa using h.2.2.1 1
        mul_mem' := h.2.1
        algebraMap_mem' := h.2.2.1
        star_mem' := h.2.2.2 }, rfl⟩

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