instStructureGroupoidOrderBot — Mathlib

English

Every StructureGroupoid contains the minimal element given by the idGroupoid.

Русский

Каждый StructureGroupoid содержит минимальный элемент, задаваемый idGroupoid.

LaTeX

$$instance instStructureGroupoidOrderBot : OrderBot (StructureGroupoid H)$$

Lean4

/-- Every structure groupoid contains the identity groupoid. -/
instance instStructureGroupoidOrderBot : OrderBot (StructureGroupoid H)
    where
  bot := idGroupoid H
  bot_le := by
    intro u f hf
    have hf : f ∈ {OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅} := hf
    simp only [singleton_union, mem_setOf_eq, mem_insert_iff] at hf
    rcases hf with hf | hf
    · rw [hf]
      apply u.id_mem
    · apply u.locality
      intro x hx
      rw [hf, mem_empty_iff_false] at hx
      exact hx.elim

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