smul_set_ae_eq

Mathlib.MeasureTheory.Group.Action

URI: https://scilib.ai/kg/mathlib#MeasureTheory.smul_set_ae_eq

← MathLib Explorer

English

For any c ∈ G, c•s =ᵐ[μ] c•t iff s =ᵐ[μ] t.

Русский

Для любого c ∈ G, c•s =ᵐ[μ] c•t эквивалентно s =ᵐ[μ] t.

LaTeX

$$$c\\;s =_{\\ae\\mu} c\\;t \\iff s =_{\\ae\\mu} t$$$

Lean4

@[to_additive (attr := simp)]
theorem smul_set_ae_eq (c : G) {s t : Set α} : c • s =ᵐ[μ] c • t ↔ s =ᵐ[μ] t := by
  simp only [Filter.eventuallyLE_antisymm_iff, smul_set_ae_le]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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