nonempty_iff — Mathlib

English

An open U ⊆ X considered as a scheme is nonempty if and only if the underlying open subset of X is nonempty.

Русский

Открытое подмножество U ⊆ X как схема непусто тогда и только тогда, когда соответствующее подмножество X непусто.

LaTeX

$$$\\text{Nonempty}(U^{toScheme}) \\iff (U : \\text{Set } X).Nonempty$$$

Lean4

@[simp]
theorem nonempty_iff : Nonempty U.toScheme ↔ (U : Set X).Nonempty :=
  by
  simp only [toScheme_carrier, SetLike.coe_sort_coe, nonempty_subtype]
  rfl

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