rfl

Mathlib.MeasureTheory.Measure.Regular

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.InnerRegularWRT.rfl

English

The case with identical predicates on domain and codomain holds automatically.

Русский

Случай, когда предикаты совпадают по обе стороны, тривиален.

LaTeX

$$$\forall \mu\ p,\ InnerRegularWRT(\mu; p, p).$$$

Lean4

theorem rfl {p : Set α → Prop} : InnerRegularWRT μ p p := fun U hU _r hr ↦ ⟨U, Subset.rfl, hU, hr⟩

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

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

Разделы

Аффилиация

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