instMinExtensionOf — Mathlib

English

There exists a minimal extension of i to f in the partially ordered set of extensions, given by a Zorn construction.

Русский

Существет минимальное продолжение i к f в частично упорядоченном множестве продолжений, получаемое через Zorn.

LaTeX

$$$ \exists\text{ extensionOf } i f\text{ that is minimal under } \le$$$

Lean4

instance : Min (ExtensionOf i f) where
  min X1
    X2 :=
    {
      X1.toLinearPMap ⊓
        X2.toLinearPMap with
      le := fun x hx =>
        (by
          rcases hx with ⟨x, rfl⟩
          refine ⟨X1.le (Set.mem_range_self _), X2.le (Set.mem_range_self _), ?_⟩
          rw [← X1.is_extension x, ← X2.is_extension x] : x ∈ X1.toLinearPMap.eqLocus X2.toLinearPMap)
      is_extension := fun _ => X1.is_extension _ }

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