hasGroupoid_of_le — Mathlib

English

If G1 has a groupoid structure on M and G2 extends G1 (G1 ≤ G2), then G2 also defines a groupoid on M.

Русский

Если на M задано групоидное пространство G1 и G2 содержит G1 (G1 ≤ G2), то G2 тоже образует группой на M.

LaTeX

$$$\text{HasGroupoid } M\ G_2\;\text{from }\text{HasGroupoid } M\ G_1\text{ and } G_1 \le G_2.$$$

Lean4

theorem hasGroupoid_of_le {G₁ G₂ : StructureGroupoid H} (h : HasGroupoid M G₁) (hle : G₁ ≤ G₂) : HasGroupoid M G₂ :=
  ⟨fun he he' ↦ hle (h.compatible he he')⟩

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