iff — Mathlib

English

The defining predicate for valuative criterion is equivalent to the conjunction of existence and uniqueness properties.

Русский

Определяющее свойство валюативного критерия эквивалентно сочетанию существования и уникальности.

LaTeX

$$$ ValuativeCriterion = Existence \\land Uniqueness $$$

Lean4

theorem iff {f : X ⟶ Y} : ValuativeCriterion f ↔ Existence f ∧ Uniqueness f :=
  by
  change (∀ _, _) ↔ (∀ _, _) ∧ (∀ _, _)
  simp_rw [← forall_and, unique_iff_subsingleton_and_nonempty, and_comm, CommSq.HasLift.iff]

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