option_iff — Mathlib

English

The algebraic independence of a sum-elimination of two families x and y is equivalent to the conjunction of the independence of x and the independence of y over the adjoin of range x.

Русский

Независимость по сумме X и Y эквивалентна сочетанию независимости X и независимости Y над ajoin{R}(range X).

LaTeX

$$$AlgebraicIndependent R (Sum.elim y x) \iff (AlgebraicIndependent R x) \land (AlgebraicIndependent (adjoin R (range x)) y)$$

Lean4

theorem option_iff {a : A} :
    AlgebraicIndependent R (fun o : Option ι ↦ o.elim a x) ↔
      AlgebraicIndependent R x ∧ Transcendental (adjoin R (range x)) a :=
  ⟨fun h ↦
    have := h.comp _ (Option.some_injective _);
    ⟨this, (this.option_iff_transcendental _).mp h⟩,
    fun h ↦ (h.1.option_iff_transcendental _).mpr h.2⟩

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