exists_eq_l — Mathlib

English

Let l: α → β and u: β → α form a Galois connection. For every b ∈ β, there exists a ∈ α with b = l(a) if and only if b = l(u(b)).

Русский

Пусть l: α → β и u: β → α образуют связь Галуа. Для каждого b ∈ β существует a ∈ α such that b = l(a) тогда и только тогда, когда b = l(u(b)).

LaTeX

$$$$ \forall b:\beta,\ (\exists a:\alpha,\ b = l(a)) \iff b = l(u(b)). $$$$

Lean4

/-- If there exists an `a` such that `b = l a`, then `a = u b` is one such element. -/
theorem exists_eq_l (b : β) : (∃ a : α, b = l a) ↔ b = l (u b) :=
  gc.dual.exists_eq_u _

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