mem_mk

Mathlib.Analysis.BoxIntegral.Partition.Basic

URI: https://scilib.ai/kg/mathlib#BoxIntegral.Prepartition.mem_mk

English

An element J belongs to the prepartition mk s h1 h2 iff J belongs to the finite set s.

Русский

Элемент J принадлежит предварительному разбиению mk s h1 h2 тогда и только тогда, когда J ∈ s.

LaTeX

$$$$ J \\in (mk\\ s\\ h_1\\ h_2 : Prepartition I) \\iff J \\in s $$$$

Lean4

@[simp]
theorem mem_mk {s h₁ h₂} : J ∈ (mk s h₁ h₂ : Prepartition I) ↔ J ∈ s :=
  Iff.rfl

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

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

Разделы

Аффилиация

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