star_coe_eq — Mathlib

English

The star of a coe-set equals the coe-set itself, under appropriate StarMemClass conditions, i.e., the star on the Set-coercion matches the underlying element.

Русский

Звезда над элементом типа-наборе равна самому этому элементу при условии, что выполняются соответствующие условия StarMemClass.

LaTeX

$$$\\\\star(s) = s.$$$

Lean4

@[simp]
theorem star_coe_eq {S α : Type*} [InvolutiveStar α] [SetLike S α] [StarMemClass S α] (s : S) : star (s : Set α) = s :=
  by
  ext x
  simp only [Set.mem_star, SetLike.mem_coe]
  exact ⟨by simpa only [star_star] using star_mem (s := s) (r := star x), star_mem⟩

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