coe_mk

Mathlib.Order.Preorder.Chain

URI: https://scilib.ai/kg/mathlib#Flag.coe_mk

English

The carrier of a flag built from a set is exactly that set.

Русский

Общее множество, порождаемое флагом из набора, равно именно этому набору.

LaTeX

$$$\\\\forall (s : Set α) (h₁ h₂), (mk s h₁ h₂ : Set α) = s$$$

Lean4

@[simp]
theorem coe_mk (s : Set α) (h₁ h₂) : (mk s h₁ h₂ : Set α) = s :=
  rfl

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

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

Разделы

Аффилиация

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