star_subset_star

Mathlib.Algebra.Star.Pointwise

URI: https://scilib.ai/kg/mathlib#Set.star_subset_star

English

For InvolutiveStar α, s⋆ ⊆ t⋆ iff s ⊆ t.

Русский

Для инволютивной звезды α верно: s⋆ ⊆ t⋆ тогда и только тогда, когда s ⊆ t.

LaTeX

$$$s^{\\star} \\subseteq t^{\\star} \\iff s \\subseteq t.$$$

Lean4

@[simp]
theorem star_subset_star [InvolutiveStar α] {s t : Set α} : s⋆ ⊆ t⋆ ↔ s ⊆ t :=
  Equiv.star.surjective.preimage_subset_preimage_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru