le_iff_nonempty_hom — Mathlib

English

For x,y ∈ X.S, x ≤ y if and only if there exists a nonempty morphism equivElements y ⟶ equivElements x.

Русский

Для x,y ∈ X.S верно: x ≤ y тогда и только тогда, когда существует непустой морфизм equivElements y ⟶ equivElements x.

LaTeX

$$$x \le y \iff \text{Nonempty} (equivElements\ y \to equivElements\ x)$$$

Lean4

theorem le_iff_nonempty_hom (x y : X.S) : x ≤ y ↔ Nonempty (equivElements y ⟶ equivElements x) :=
  by
  rw [le_iff]
  constructor
  · rintro ⟨f, hf⟩
    exact ⟨⟨f.op, hf⟩⟩
  · rintro ⟨f, hf⟩
    exact ⟨f.unop, hf⟩

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