le_iff

Mathlib.Geometry.Manifold.ChartedSpace

URI: https://scilib.ai/kg/mathlib#StructureGroupoid.le_iff

English

A preorder relation on StructureGroupoid corresponds to membership inequalities.

Русский

К отношению предшествования в StructureGroupoid соответствует неравенствам по членству.

LaTeX

$$G1 ≤ G2 ↔ ∀ e, e ∈ G1 → e ∈ G2$$

Lean4

theorem le_iff {G₁ G₂ : StructureGroupoid H} : G₁ ≤ G₂ ↔ ∀ e, e ∈ G₁ → e ∈ G₂ :=
  Iff.rfl

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

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

Разделы

Аффилиация

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