Commit 2026-01-03 17:21 4ffa0474

View on Github →

refactor: rename ≤ᵥ to vle and <ᵥ to vlt (#33040) This makes room to later add =ᵥ or veq defined as AntisymmRel (· ≤ᵥ ·).

Estimated changes

deleted theorem Valuation.one_rel_iff
deleted theorem Valuation.one_srel_iff
added theorem Valuation.one_vle_iff
added theorem Valuation.one_vlt_iff
deleted theorem Valuation.rel_iff_le
deleted theorem Valuation.rel_one_iff
deleted theorem Valuation.srel_iff_lt
deleted theorem Valuation.srel_one_iff
added theorem Valuation.vle_iff_le
added theorem Valuation.vle_one_iff
added theorem Valuation.vlt_iff_lt
added theorem Valuation.vlt_one_iff
deleted theorem ValuativeRel.SRel.rel
deleted theorem ValuativeRel.SRel.trans
deleted def ValuativeRel.SRel
deleted theorem ValuativeRel.div_rel_iff
deleted theorem ValuativeRel.inv_rel_one
deleted theorem ValuativeRel.inv_srel_one
deleted theorem ValuativeRel.mul_rel_mul
deleted theorem ValuativeRel.mul_srel_mul
deleted theorem ValuativeRel.not_srel_iff
added theorem ValuativeRel.not_vle
added theorem ValuativeRel.not_vlt
deleted theorem ValuativeRel.one_rel_inv
deleted theorem ValuativeRel.one_srel_inv
deleted theorem ValuativeRel.pow_rel_pow
deleted theorem ValuativeRel.pow_srel_pow
deleted theorem ValuativeRel.rel_div_iff
deleted theorem ValuativeRel.rel_mul_left
deleted theorem ValuativeRel.rel_refl
deleted theorem ValuativeRel.rel_rfl
deleted theorem ValuativeRel.rel_trans'
deleted theorem ValuativeRel.rel_zero_iff
modified theorem ValuativeRel.srel_iff
added theorem ValuativeRel.vle_refl
added theorem ValuativeRel.vle_rfl
added theorem ValuativeRel.vlt.trans
added theorem ValuativeRel.vlt.vle
added def ValuativeRel.vlt
deleted theorem ValuativeRel.zero_rel
added theorem ValuativeRel.zero_vle