lt_largerSubobject — Mathlib

English

If A is a proper subobject of X, then A is strictly contained in largerSubobject hG A.

Русский

Если A — действительный подобъект X, то A строго меньше largerSubobject hG A.

LaTeX

$$$A < largerSubobject hG A$$$

Lean4

theorem lt_largerSubobject (A : Subobject X) (hA : A ≠ ⊤) : A < largerSubobject hG A :=
  by
  dsimp only [largerSubobject]
  rw [dif_neg hA]
  exact (exists_larger_subobject hG A hA).choose_spec.choose

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