pullSub_adjunction — Mathlib

English

For any S,T and x, pullSub S x ≤ T if and only if S ≤ subAt T x.

Русский

Для произвольных S, T и x выполняется: pullSub S x ≤ T тогда и только если S ≤ subAt T x.

LaTeX

$$$ pullSub S x \le T \iff S \le subAt T x $$$

Lean4

theorem pullSub_adjunction (S T : tree A) (x : List A) : pullSub S x ≤ T ↔ S ≤ subAt T x
    where
  mp _ := by rw [← subAt_pullSub S x]; gcongr
  mpr _ := le_trans (by gcongr) (pullSub_subAt T x)

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